Skip to content

Commit

Permalink
Generate code for GH-551
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-actions
github-actions[bot] committed Aug 26, 2024
1 parent 2e2159f commit f12f834
Show file tree
Hide file tree
Showing 65 changed files with 89,914 additions and 91,070 deletions.
3,136 changes: 1,633 additions & 1,503 deletions generated/MAlonzo/Code/Axiom/Set.hs
View file

Large diffs are not rendered by default.

150 changes: 75 additions & 75 deletions generated/MAlonzo/Code/Axiom/Set/Factor.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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'__668 (coe v0) v2 v3
-- Axiom.Set.Factor._._≡ᵉ_
d__'8801''7497'__20 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
Expand All @@ -47,52 +47,52 @@ d__'8801''7497'__20 = erased
d_FinSet_32 :: MAlonzo.Code.Axiom.Set.T_Theory_82 -> () -> ()
d_FinSet_32 = erased
-- Axiom.Set.Factor._.disjoint
d_disjoint_44 ::
d_disjoint_46 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() -> AgdaAny -> AgdaAny -> ()
d_disjoint_44 = erased
d_disjoint_46 = erased
-- Axiom.Set.Factor._.finite
d_finite_48 ::
d_finite_50 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 -> () -> AgdaAny -> ()
d_finite_48 = erased
d_finite_50 = erased
-- Axiom.Set.Factor._ᶠ
d__'7584'_310 ::
d__'7584'_312 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d__'7584'_310 ~v0 ~v1 v2 v3 = du__'7584'_310 v2 v3
du__'7584'_310 ::
d__'7584'_312 ~v0 ~v1 v2 v3 = du__'7584'_312 v2 v3
du__'7584'_312 ::
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du__'7584'_310 v0 v1
du__'7584'_312 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''_320 ::
d_'8746''45'preserves'45'finite''_322 ::
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''_320 v0 ~v1 v2 v3 v4 v5
= du_'8746''45'preserves'45'finite''_320 v0 v2 v3 v4 v5
du_'8746''45'preserves'45'finite''_320 ::
d_'8746''45'preserves'45'finite''_322 v0 ~v1 v2 v3 v4 v5
= du_'8746''45'preserves'45'finite''_322 v0 v2 v3 v4 v5
du_'8746''45'preserves'45'finite''_322 ::
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''_320 v0 v1 v2 v3 v4
du_'8746''45'preserves'45'finite''_322 v0 v1 v2 v3 v4
= coe
MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_706
MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_708
(coe v0) (coe v1) (coe v2) (coe v3) (coe v4)
-- Axiom.Set.Factor.Factor.factor
d_factor_342 ::
d_factor_344 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -103,19 +103,19 @@ d_factor_342 ::
(AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
d_factor_342 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_342 v4 v6
du_factor_342 ::
d_factor_344 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_344 v4 v6
du_factor_344 ::
([AgdaAny] -> AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
du_factor_342 v0 v1
du_factor_344 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_346 ::
d_factor'45'cong_348 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -128,17 +128,17 @@ d_factor'45'cong_346 ::
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_346 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
= du_factor'45'cong_346 v5 v6 v7 v8
du_factor'45'cong_346 ::
d_factor'45'cong_348 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
= du_factor'45'cong_348 v5 v6 v7 v8
du_factor'45'cong_348 ::
([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_346 v0 v1 v2 v3
du_factor'45'cong_348 v0 v1 v2 v3
= case coe v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
-> case coe v5 of
Expand Down Expand Up @@ -186,7 +186,7 @@ du_factor'45'cong_346 v0 v1 v2 v3
(coe
MAlonzo.Code.Function.Bundles.d_to_1724
(coe
MAlonzo.Code.Axiom.Set.Properties.du_'8801''7497''8660''8801''7497'''_242)
MAlonzo.Code.Axiom.Set.Properties.du_'8801''7497''8660''8801''7497'''_244)
v3 v12))
(coe
MAlonzo.Code.Function.Related.Propositional.du_SK'45'sym_168
Expand All @@ -198,7 +198,7 @@ du_factor'45'cong_346 v0 v1 v2 v3
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
-- Axiom.Set.Factor.Factor.factor-∪
d_factor'45''8746'_382 ::
d_factor'45''8746'_384 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -214,27 +214,27 @@ d_factor'45''8746'_382 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
d_factor'45''8746'_382 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
= du_factor'45''8746'_382 v7 v8 v9 v10 v11
du_factor'45''8746'_382 ::
d_factor'45''8746'_384 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
= du_factor'45''8746'_384 v7 v8 v9 v10 v11
du_factor'45''8746'_384 ::
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
du_factor'45''8746'_382 v0 v1 v2 v3 v4
du_factor'45''8746'_384 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'_310 (coe v0) (coe v2))))
(coe du__'7584'_312 (coe v0) (coe v2))))
(MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
(coe
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
(coe du__'7584'_310 (coe v1) (coe v3))))
(coe du__'7584'_312 (coe v1) (coe v3))))
-- Axiom.Set.Factor.FactorUnique.f-cong'
d_f'45'cong''_410 ::
d_f'45'cong''_412 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -249,9 +249,9 @@ d_f'45'cong''_410 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
(AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
AgdaAny
d_f'45'cong''_410 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
= du_f'45'cong''_410 v6 v7 v8 v9
du_f'45'cong''_410 ::
d_f'45'cong''_412 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
= du_f'45'cong''_412 v6 v7 v8 v9
du_f'45'cong''_412 ::
(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 ->
Expand All @@ -260,7 +260,7 @@ du_f'45'cong''_410 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
(AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
AgdaAny
du_f'45'cong''_410 v0 v1 v2 v3
du_f'45'cong''_412 v0 v1 v2 v3
= coe
v0 v1 v2
(coe
Expand All @@ -271,7 +271,7 @@ du_f'45'cong''_410 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'Σ_418 ::
d_deduplicate'45'Σ_420 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -283,12 +283,12 @@ d_deduplicate'45'Σ_418 ::
MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
AgdaAny) ->
[AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_deduplicate'45'Σ_418 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
= du_deduplicate'45'Σ_418 v3 v7
du_deduplicate'45'Σ_418 ::
d_deduplicate'45'Σ_420 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
= du_deduplicate'45'Σ_420 v3 v7
du_deduplicate'45'Σ_420 ::
MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
[AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_deduplicate'45'Σ_418 v0 v1
du_deduplicate'45'Σ_420 v0 v1
= coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
Expand All @@ -299,7 +299,7 @@ du_deduplicate'45'Σ_418 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_422 ::
d_ext_424 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -311,15 +311,15 @@ d_ext_422 ::
MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
AgdaAny) ->
[AgdaAny] -> AgdaAny
d_ext_422 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_422 v3 v5 v7
du_ext_422 ::
d_ext_424 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_424 v3 v5 v7
du_ext_424 ::
MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
[AgdaAny] -> AgdaAny
du_ext_422 v0 v1 v2
= coe v1 (coe du_deduplicate'45'Σ_418 (coe v0) (coe v2))
du_ext_424 v0 v1 v2
= coe v1 (coe du_deduplicate'45'Σ_420 (coe v0) (coe v2))
-- Axiom.Set.Factor.FactorUnique.ext-cong
d_ext'45'cong_428 ::
d_ext'45'cong_430 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -334,9 +334,9 @@ d_ext'45'cong_428 ::
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
AgdaAny
d_ext'45'cong_428 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
= du_ext'45'cong_428 v3 v6 v7 v8 v9
du_ext'45'cong_428 ::
d_ext'45'cong_430 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
= du_ext'45'cong_430 v3 v6 v7 v8 v9
du_ext'45'cong_430 ::
MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
Expand All @@ -346,9 +346,9 @@ du_ext'45'cong_428 ::
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
AgdaAny
du_ext'45'cong_428 v0 v1 v2 v3 v4
du_ext'45'cong_430 v0 v1 v2 v3 v4
= coe
du_f'45'cong''_410 (coe v1)
du_f'45'cong''_412 (coe v1)
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(coe
Expand Down Expand Up @@ -408,7 +408,7 @@ du_ext'45'cong_428 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_444 ::
d_factor_446 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -420,15 +420,15 @@ d_factor_444 ::
MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
AgdaAny) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
d_factor_444 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_444 v3 v5
du_factor_444 ::
d_factor_446 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_446 v3 v5
du_factor_446 ::
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_444 v0 v1
= coe du_factor_342 (coe du_ext_422 (coe v0) (coe v1))
du_factor_446 v0 v1
= coe du_factor_344 (coe du_ext_424 (coe v0) (coe v1))
-- Axiom.Set.Factor.FactorUnique._.factor-cong
d_factor'45'cong_446 ::
d_factor'45'cong_448 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -442,9 +442,9 @@ d_factor'45'cong_446 ::
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_446 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
= du_factor'45'cong_446 v3 v6
du_factor'45'cong_446 ::
d_factor'45'cong_448 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
= du_factor'45'cong_448 v3 v6
du_factor'45'cong_448 ::
MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
Expand All @@ -453,11 +453,11 @@ du_factor'45'cong_446 ::
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_446 v0 v1
du_factor'45'cong_448 v0 v1
= coe
du_factor'45'cong_346 (coe du_ext'45'cong_428 (coe v0) (coe v1))
du_factor'45'cong_348 (coe du_ext'45'cong_430 (coe v0) (coe v1))
-- Axiom.Set.Factor.FactorUnique._.factor-∪
d_factor'45''8746'_448 ::
d_factor'45''8746'_450 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -474,19 +474,19 @@ d_factor'45''8746'_448 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
d_factor'45''8746'_448 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
= du_factor'45''8746'_448
du_factor'45''8746'_448 ::
d_factor'45''8746'_450 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
= du_factor'45''8746'_450
du_factor'45''8746'_450 ::
(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'_448 v0 v1 v2 v3 v4 v5
= coe du_factor'45''8746'_382 v1 v2 v3 v4 v5
du_factor'45''8746'_450 v0 v1 v2 v3 v4 v5
= coe du_factor'45''8746'_384 v1 v2 v3 v4 v5
-- Axiom.Set.Factor.FactorUnique.factor-∪'
d_factor'45''8746'''_464 ::
d_factor'45''8746'''_466 ::
MAlonzo.Code.Axiom.Set.T_Theory_82 ->
() ->
() ->
Expand All @@ -512,10 +512,10 @@ d_factor'45''8746'''_464 ::
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny) ->
AgdaAny
d_factor'45''8746'''_464 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
d_factor'45''8746'''_466 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
v10 v11 ~v12 v13
= du_factor'45''8746'''_464 v10 v11 v13
du_factor'45''8746'''_464 ::
= du_factor'45''8746'''_466 v10 v11 v13
du_factor'45''8746'''_466 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
([AgdaAny] ->
Expand All @@ -525,7 +525,7 @@ du_factor'45''8746'''_464 ::
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny) ->
AgdaAny
du_factor'45''8746'''_464 v0 v1 v2
du_factor'45''8746'''_466 v0 v1 v2
= case coe v0 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
-> case coe v1 of
Expand Down
Loading

0 comments on commit f12f834

Please sign in to comment.