{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Data.Unit.Properties where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Unit.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary
d_'8868''45'irrelevant_6 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8868''45'irrelevant_6 :: T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12
d_'8868''45'irrelevant_6 = T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12
forall a. a
erased
d__'8799'__8 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__8 :: T_'8868'_6 -> T_'8868'_6 -> T_Dec_32
d__'8799'__8 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T_Dec_32
du__'8799'__8
du__'8799'__8 :: MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8799'__8 :: T_Dec_32
du__'8799'__8
= (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
forall a. a
erased)
d_'8801''45'setoid_10 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_10 :: T_Setoid_44
d_'8801''45'setoid_10
= T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250
d_'8801''45'decSetoid_12 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_12 :: T_DecSetoid_84
d_'8801''45'decSetoid_12
= ((Any -> Any -> T_Dec_32) -> T_DecSetoid_84)
-> (Any -> Any -> Any) -> T_DecSetoid_84
forall a b. a -> b
coe
(Any -> Any -> T_Dec_32) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_254
(\ Any
v0 Any
v1 -> T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
du__'8799'__8)
d_'8801''45'total_14 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8801''45'total_14 :: T_'8868'_6 -> T_'8868'_6 -> T__'8846'__30
d_'8801''45'total_14 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T__'8846'__30
du_'8801''45'total_14
du_'8801''45'total_14 :: MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8801''45'total_14 :: T__'8846'__30
du_'8801''45'total_14
= (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
forall a. a
erased
d_'8801''45'antisym_16 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8801''45'antisym_16 :: T_'8868'_6
-> T_'8868'_6 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12
d_'8801''45'antisym_16 = T_'8868'_6
-> T_'8868'_6 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8801''45'isPreorder_20 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8801''45'isPreorder_20 :: T_IsPreorder_70
d_'8801''45'isPreorder_20
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70)
-> Any -> Any -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2)) Any
forall a. a
erased
d_'8801''45'isPartialOrder_24 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8801''45'isPartialOrder_24 :: T_IsPartialOrder_162
d_'8801''45'isPartialOrder_24
= (T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_162)
-> Any -> Any -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8801''45'isPreorder_20) Any
forall a. a
erased
d_'8801''45'isTotalOrder_26 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_'8801''45'isTotalOrder_26 :: T_IsTotalOrder_384
d_'8801''45'isTotalOrder_26
= (T_IsPartialOrder_162
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_384)
-> Any -> (Any -> Any -> Any) -> T_IsTotalOrder_384
forall a b. a -> b
coe
T_IsPartialOrder_162
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
(T_IsPartialOrder_162 -> Any
forall a b. a -> b
coe T_IsPartialOrder_162
d_'8801''45'isPartialOrder_24)
(\ Any
v0 Any
v1 -> T__'8846'__30 -> Any
forall a b. a -> b
coe T__'8846'__30
du_'8801''45'total_14)
d_'8801''45'isDecTotalOrder_28 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_'8801''45'isDecTotalOrder_28 :: T_IsDecTotalOrder_434
d_'8801''45'isDecTotalOrder_28
= (T_IsTotalOrder_384
-> (Any -> Any -> T_Dec_32)
-> (Any -> Any -> T_Dec_32)
-> T_IsDecTotalOrder_434)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDecTotalOrder_434
forall a b. a -> b
coe
T_IsTotalOrder_384
-> (Any -> Any -> T_Dec_32)
-> (Any -> Any -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
(T_IsTotalOrder_384 -> Any
forall a b. a -> b
coe T_IsTotalOrder_384
d_'8801''45'isTotalOrder_26) (\ Any
v0 Any
v1 -> T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
du__'8799'__8)
(\ Any
v0 Any
v1 -> T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
du__'8799'__8)
d_'8801''45'poset_30 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8801''45'poset_30 :: T_Poset_282
d_'8801''45'poset_30
= (T_IsPartialOrder_162 -> T_Poset_282)
-> T_IsPartialOrder_162 -> T_Poset_282
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
T_IsPartialOrder_162
d_'8801''45'isPartialOrder_24
d_'8801''45'decTotalOrder_32 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
d_'8801''45'decTotalOrder_32 :: T_DecTotalOrder_740
d_'8801''45'decTotalOrder_32
= (T_IsDecTotalOrder_434 -> T_DecTotalOrder_740)
-> T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
forall a b. a -> b
coe
T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_14337
T_IsDecTotalOrder_434
d_'8801''45'isDecTotalOrder_28
d_'8804''45'reflexive_34 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10
d_'8804''45'reflexive_34 :: T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12 -> T__'8804'__10
d_'8804''45'reflexive_34 = T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12 -> T__'8804'__10
forall a. a
erased
d_'8804''45'trans_36 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10
d_'8804''45'trans_36 :: T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T__'8804'__10
-> T__'8804'__10
-> T__'8804'__10
d_'8804''45'trans_36 = T_'8868'_6
-> T_'8868'_6
-> T_'8868'_6
-> T__'8804'__10
-> T__'8804'__10
-> T__'8804'__10
forall a. a
erased
d_'8804''45'antisym_38 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Unit.Base.T__'8804'__10 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''45'antisym_38 :: T_'8868'_6
-> T_'8868'_6 -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
d_'8804''45'antisym_38 = T_'8868'_6
-> T_'8868'_6 -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
forall a. a
erased
d_'8804''45'total_40 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8804''45'total_40 :: T_'8868'_6 -> T_'8868'_6 -> T__'8846'__30
d_'8804''45'total_40 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T__'8846'__30
du_'8804''45'total_40
du_'8804''45'total_40 :: MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8804''45'total_40 :: T__'8846'__30
du_'8804''45'total_40
= (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
forall a. a
erased
d__'8804''63'__42 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8804''63'__42 :: T_'8868'_6 -> T_'8868'_6 -> T_Dec_32
d__'8804''63'__42 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T_Dec_32
du__'8804''63'__42
du__'8804''63'__42 :: MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8804''63'__42 :: T_Dec_32
du__'8804''63'__42
= (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
forall a. a
erased)
d_'8804''45'isPreorder_44 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''45'isPreorder_44 :: T_IsPreorder_70
d_'8804''45'isPreorder_44
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70)
-> Any -> Any -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
Any
forall a. a
erased Any
forall a. a
erased
d_'8804''45'isPartialOrder_46 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8804''45'isPartialOrder_46 :: T_IsPartialOrder_162
d_'8804''45'isPartialOrder_46
= (T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_162)
-> Any -> Any -> T_IsPartialOrder_162
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8804''45'isPreorder_44) Any
forall a. a
erased
d_'8804''45'isTotalOrder_48 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_'8804''45'isTotalOrder_48 :: T_IsTotalOrder_384
d_'8804''45'isTotalOrder_48
= (T_IsPartialOrder_162
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_384)
-> Any -> (Any -> Any -> Any) -> T_IsTotalOrder_384
forall a b. a -> b
coe
T_IsPartialOrder_162
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
(T_IsPartialOrder_162 -> Any
forall a b. a -> b
coe T_IsPartialOrder_162
d_'8804''45'isPartialOrder_46)
(\ Any
v0 Any
v1 -> T__'8846'__30 -> Any
forall a b. a -> b
coe T__'8846'__30
du_'8804''45'total_40)
d_'8804''45'isDecTotalOrder_50 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_'8804''45'isDecTotalOrder_50 :: T_IsDecTotalOrder_434
d_'8804''45'isDecTotalOrder_50
= (T_IsTotalOrder_384
-> (Any -> Any -> T_Dec_32)
-> (Any -> Any -> T_Dec_32)
-> T_IsDecTotalOrder_434)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDecTotalOrder_434
forall a b. a -> b
coe
T_IsTotalOrder_384
-> (Any -> Any -> T_Dec_32)
-> (Any -> Any -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
(T_IsTotalOrder_384 -> Any
forall a b. a -> b
coe T_IsTotalOrder_384
d_'8804''45'isTotalOrder_48) (\ Any
v0 Any
v1 -> T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
du__'8799'__8)
(\ Any
v0 Any
v1 -> T_Dec_32 -> Any
forall a b. a -> b
coe T_Dec_32
du__'8804''63'__42)
d_'8804''45'poset_52 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8804''45'poset_52 :: T_Poset_282
d_'8804''45'poset_52
= (T_IsPartialOrder_162 -> T_Poset_282)
-> T_IsPartialOrder_162 -> T_Poset_282
forall a b. a -> b
coe
T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
T_IsPartialOrder_162
d_'8804''45'isPartialOrder_46
d_'8804''45'decTotalOrder_54 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
d_'8804''45'decTotalOrder_54 :: T_DecTotalOrder_740
d_'8804''45'decTotalOrder_54
= (T_IsDecTotalOrder_434 -> T_DecTotalOrder_740)
-> T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
forall a b. a -> b
coe
T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_14337
T_IsDecTotalOrder_434
d_'8804''45'isDecTotalOrder_50