formal-ledger-specification commit 6530562dd8d9fbb8c499562c548240066e…

…301e6b
input-output-hk · May 8, 2024 · e1e0a33 · e1e0a33
1 parent a339581
commit e1e0a33
Show file tree

Hide file tree

Showing 33 changed files with 42,213 additions and 33,046 deletions.
diff --git a/MAlonzo/Code/Axiom/Set.hs b/MAlonzo/Code/Axiom/Set.hs
diff --git a/MAlonzo/Code/Axiom/Set/Factor.hs b/MAlonzo/Code/Axiom/Set/Factor.hs
@@ -37,7 +37,7 @@ d__'8746'__18 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () -> AgdaAny -> AgdaAny -> AgdaAny
 d__'8746'__18 v0 v1 v2 v3
-  = coe MAlonzo.Code.Axiom.Set.du__'8746'__662 (coe v0) v2 v3
+  = coe MAlonzo.Code.Axiom.Set.du__'8746'__666 (coe v0) v2 v3
 -- Axiom.Set.Factor._._≡ᵉ_
 d__'8801''7497'__20 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
@@ -56,43 +56,43 @@ d_finite_48 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 -> () -> AgdaAny -> ()
 d_finite_48 = erased
 -- Axiom.Set.Factor._ᶠ
-d__'7584'_286 ::
+d__'7584'_288 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d__'7584'_286 ~v0 ~v1 v2 v3 = du__'7584'_286 v2 v3
-du__'7584'_286 ::
+d__'7584'_288 ~v0 ~v1 v2 v3 = du__'7584'_288 v2 v3
+du__'7584'_288 ::
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du__'7584'_286 v0 v1
+du__'7584'_288 v0 v1
   = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0) (coe v1)
 -- Axiom.Set.Factor.∪-preserves-finite'
-d_'8746''45'preserves'45'finite''_296 ::
+d_'8746''45'preserves'45'finite''_298 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d_'8746''45'preserves'45'finite''_296 v0 ~v1 v2 v3 v4 v5
-  = du_'8746''45'preserves'45'finite''_296 v0 v2 v3 v4 v5
-du_'8746''45'preserves'45'finite''_296 ::
+d_'8746''45'preserves'45'finite''_298 v0 ~v1 v2 v3 v4 v5
+  = du_'8746''45'preserves'45'finite''_298 v0 v2 v3 v4 v5
+du_'8746''45'preserves'45'finite''_298 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du_'8746''45'preserves'45'finite''_296 v0 v1 v2 v3 v4
+du_'8746''45'preserves'45'finite''_298 v0 v1 v2 v3 v4
   = coe
-      MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_616
+      MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_618
       (coe v0) (coe v1) (coe v2) (coe v3) (coe v4)
 -- Axiom.Set.Factor.Factor.factor
-d_factor_318 ::
+d_factor_320 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -103,19 +103,19 @@ d_factor_318 ::
    (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor_318 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_318 v4 v6
-du_factor_318 ::
+d_factor_320 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_320 v4 v6
+du_factor_320 ::
   ([AgdaAny] -> AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor_318 v0 v1
+du_factor_320 v0 v1
   = case coe v1 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
         -> case coe v3 of
              MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5 -> coe v0 v4
              _ -> MAlonzo.RTE.mazUnreachableError
       _ -> MAlonzo.RTE.mazUnreachableError
 -- Axiom.Set.Factor.Factor.factor-cong
-d_factor'45'cong_322 ::
+d_factor'45'cong_324 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -128,17 +128,17 @@ d_factor'45'cong_322 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor'45'cong_322 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
-  = du_factor'45'cong_322 v5 v6 v7 v8
-du_factor'45'cong_322 ::
+d_factor'45'cong_324 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
+  = du_factor'45'cong_324 v5 v6 v7 v8
+du_factor'45'cong_324 ::
   ([AgdaAny] ->
    [AgdaAny] ->
    (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor'45'cong_322 v0 v1 v2 v3
+du_factor'45'cong_324 v0 v1 v2 v3
   = case coe v1 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
         -> case coe v5 of
@@ -186,7 +186,7 @@ du_factor'45'cong_322 v0 v1 v2 v3
                                           (coe
                                              MAlonzo.Code.Function.Bundles.d_to_1724
                                              (coe
-                                                MAlonzo.Code.Axiom.Set.Properties.du_'8801''7497''8660''8801''7497'''_246)
+                                                MAlonzo.Code.Axiom.Set.Properties.du_'8801''7497''8660''8801''7497'''_248)
                                              v3 v12))
                                        (coe
                                           MAlonzo.Code.Function.Related.Propositional.du_SK'45'sym_168
@@ -198,7 +198,7 @@ du_factor'45'cong_322 v0 v1 v2 v3
              _ -> MAlonzo.RTE.mazUnreachableError
       _ -> MAlonzo.RTE.mazUnreachableError
 -- Axiom.Set.Factor.Factor.factor-∪
-d_factor'45''8746'_358 ::
+d_factor'45''8746'_360 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -214,27 +214,27 @@ d_factor'45''8746'_358 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-d_factor'45''8746'_358 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
-  = du_factor'45''8746'_358 v7 v8 v9 v10 v11
-du_factor'45''8746'_358 ::
+d_factor'45''8746'_360 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
+  = du_factor'45''8746'_360 v7 v8 v9 v10 v11
+du_factor'45''8746'_360 ::
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-du_factor'45''8746'_358 v0 v1 v2 v3 v4
+du_factor'45''8746'_360 v0 v1 v2 v3 v4
   = coe
       v4
       (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
          (coe
             MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
-            (coe du__'7584'_286 (coe v0) (coe v2))))
+            (coe du__'7584'_288 (coe v0) (coe v2))))
       (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
          (coe
             MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
-            (coe du__'7584'_286 (coe v1) (coe v3))))
+            (coe du__'7584'_288 (coe v1) (coe v3))))
 -- Axiom.Set.Factor.FactorUnique.f-cong'
-d_f'45'cong''_386 ::
+d_f'45'cong''_388 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -249,9 +249,9 @@ d_f'45'cong''_386 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-d_f'45'cong''_386 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
-  = du_f'45'cong''_386 v6 v7 v8 v9
-du_f'45'cong''_386 ::
+d_f'45'cong''_388 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
+  = du_f'45'cong''_388 v6 v7 v8 v9
+du_f'45'cong''_388 ::
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
@@ -260,7 +260,7 @@ du_f'45'cong''_386 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-du_f'45'cong''_386 v0 v1 v2 v3
+du_f'45'cong''_388 v0 v1 v2 v3
   = coe
       v0 v1 v2
       (coe
@@ -271,7 +271,7 @@ du_f'45'cong''_386 v0 v1 v2 v3
             MAlonzo.Code.Data.List.Relation.Unary.Unique.Propositional.Properties.WithK.du_unique'8743'set'8658'bag_64
             (coe v3)))
 -- Axiom.Set.Factor.FactorUnique.deduplicate-Σ
-d_deduplicate'45'Σ_394 ::
+d_deduplicate'45'Σ_396 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -283,12 +283,12 @@ d_deduplicate'45'Σ_394 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d_deduplicate'45'Σ_394 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
-  = du_deduplicate'45'Σ_394 v3 v7
-du_deduplicate'45'Σ_394 ::
+d_deduplicate'45'Σ_396 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
+  = du_deduplicate'45'Σ_396 v3 v7
+du_deduplicate'45'Σ_396 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du_deduplicate'45'Σ_394 v0 v1
+du_deduplicate'45'Σ_396 v0 v1
   = coe
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
       (coe
@@ -298,7 +298,7 @@ du_deduplicate'45'Σ_394 v0 v1
          MAlonzo.Code.Data.List.Relation.Unary.Unique.DecPropositional.Properties.du_deduplicate'45''33'_42
          (MAlonzo.Code.Class.DecEq.Core.d__'8799'__16 (coe v0)) v1)
 -- Axiom.Set.Factor.FactorUnique.ext
-d_ext_398 ::
+d_ext_400 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -310,15 +310,15 @@ d_ext_398 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   [AgdaAny] -> AgdaAny
-d_ext_398 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_398 v3 v5 v7
-du_ext_398 ::
+d_ext_400 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_400 v3 v5 v7
+du_ext_400 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
   [AgdaAny] -> AgdaAny
-du_ext_398 v0 v1 v2
-  = coe v1 (coe du_deduplicate'45'Σ_394 (coe v0) (coe v2))
+du_ext_400 v0 v1 v2
+  = coe v1 (coe du_deduplicate'45'Σ_396 (coe v0) (coe v2))
 -- Axiom.Set.Factor.FactorUnique.ext-cong
-d_ext'45'cong_404 ::
+d_ext'45'cong_406 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -333,9 +333,9 @@ d_ext'45'cong_404 ::
   [AgdaAny] ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-d_ext'45'cong_404 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
-  = du_ext'45'cong_404 v3 v6 v7 v8 v9
-du_ext'45'cong_404 ::
+d_ext'45'cong_406 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
+  = du_ext'45'cong_406 v3 v6 v7 v8 v9
+du_ext'45'cong_406 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
@@ -345,9 +345,9 @@ du_ext'45'cong_404 ::
   [AgdaAny] ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-du_ext'45'cong_404 v0 v1 v2 v3 v4
+du_ext'45'cong_406 v0 v1 v2 v3 v4
   = coe
-      du_f'45'cong''_386 (coe v1)
+      du_f'45'cong''_388 (coe v1)
       (coe
          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
          (coe
@@ -405,7 +405,7 @@ du_ext'45'cong_404 v0 v1 v2 v3 v4
                     MAlonzo.Code.Data.List.Ext.Properties.du_'8712''45'dedup_178
                     (coe v0) (coe v2) (coe v5)))))
 -- Axiom.Set.Factor.FactorUnique._.factor
-d_factor_420 ::
+d_factor_422 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -417,15 +417,15 @@ d_factor_420 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor_420 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_420 v3 v5
-du_factor_420 ::
+d_factor_422 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_422 v3 v5
+du_factor_422 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor_420 v0 v1
-  = coe du_factor_318 (coe du_ext_398 (coe v0) (coe v1))
+du_factor_422 v0 v1
+  = coe du_factor_320 (coe du_ext_400 (coe v0) (coe v1))
 -- Axiom.Set.Factor.FactorUnique._.factor-cong
-d_factor'45'cong_422 ::
+d_factor'45'cong_424 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -439,9 +439,9 @@ d_factor'45'cong_422 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor'45'cong_422 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
-  = du_factor'45'cong_422 v3 v6
-du_factor'45'cong_422 ::
+d_factor'45'cong_424 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
+  = du_factor'45'cong_424 v3 v6
+du_factor'45'cong_424 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
@@ -450,11 +450,11 @@ du_factor'45'cong_422 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor'45'cong_422 v0 v1
+du_factor'45'cong_424 v0 v1
   = coe
-      du_factor'45'cong_322 (coe du_ext'45'cong_404 (coe v0) (coe v1))
+      du_factor'45'cong_324 (coe du_ext'45'cong_406 (coe v0) (coe v1))
 -- Axiom.Set.Factor.FactorUnique._.factor-∪
-d_factor'45''8746'_424 ::
+d_factor'45''8746'_426 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -471,19 +471,19 @@ d_factor'45''8746'_424 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-d_factor'45''8746'_424 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
-  = du_factor'45''8746'_424
-du_factor'45''8746'_424 ::
+d_factor'45''8746'_426 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
+  = du_factor'45''8746'_426
+du_factor'45''8746'_426 ::
   (AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-du_factor'45''8746'_424 v0 v1 v2 v3 v4 v5
-  = coe du_factor'45''8746'_358 v1 v2 v3 v4 v5
+du_factor'45''8746'_426 v0 v1 v2 v3 v4 v5
+  = coe du_factor'45''8746'_360 v1 v2 v3 v4 v5
 -- Axiom.Set.Factor.FactorUnique.factor-∪'
-d_factor'45''8746'''_440 ::
+d_factor'45''8746'''_442 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -509,10 +509,10 @@ d_factor'45''8746'''_440 ::
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny) ->
   AgdaAny
-d_factor'45''8746'''_440 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
+d_factor'45''8746'''_442 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                          v10 v11 ~v12 v13
-  = du_factor'45''8746'''_440 v10 v11 v13
-du_factor'45''8746'''_440 ::
+  = du_factor'45''8746'''_442 v10 v11 v13
+du_factor'45''8746'''_442 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] ->
@@ -522,7 +522,7 @@ du_factor'45''8746'''_440 ::
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny) ->
   AgdaAny
-du_factor'45''8746'''_440 v0 v1 v2
+du_factor'45''8746'''_442 v0 v1 v2
   = case coe v0 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
         -> case coe v1 of