{-# 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.Relation.Binary.Properties.Preorder 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Structures
d_invIsPreorder_64 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_invIsPreorder_64 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_IsPreorder_70
d_invIsPreorder_64 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 T_Preorder_132
v3
du_invIsPreorder_64 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_invIsPreorder_64 :: T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 T_Preorder_132
v0
= (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_IsPreorder_70 -> T_IsEquivalence_26) -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 ->
(T_IsPreorder_70 -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82
(T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v2
Any
v1
((T_IsEquivalence_26 -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsEquivalence_26 -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
(T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
((T_Preorder_132 -> T_IsPreorder_70) -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0)))
Any
v1 Any
v2 Any
v3)))
((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 ->
(T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v3
Any
v2 Any
v1 Any
v5 Any
v4))
d_invPreorder_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_invPreorder_66 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_invPreorder_66 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3 = T_Preorder_132 -> T_Preorder_132
du_invPreorder_66 T_Preorder_132
v3
du_invPreorder_66 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_invPreorder_66 :: T_Preorder_132 -> T_Preorder_132
du_invPreorder_66 T_Preorder_132
v0
= (T_IsPreorder_70 -> T_Preorder_132) -> Any -> T_Preorder_132
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe T_Preorder_132 -> T_IsPreorder_70
du_invIsPreorder_64 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
d_InducedEquivalence_68 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence_68 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Setoid_44
d_InducedEquivalence_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
= T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_68 T_Preorder_132
v3
du_InducedEquivalence_68 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence_68 :: T_Preorder_132 -> T_Setoid_44
du_InducedEquivalence_68 T_Preorder_132
v0
= (T_IsEquivalence_26 -> T_Setoid_44) -> Any -> T_Setoid_44
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_727
(((Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_743
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 ->
(Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_IsPreorder_70 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
(Any -> Any
forall a b. a -> b
coe Any
v1))
((T_IsPreorder_70 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
((T_Preorder_132 -> T_IsPreorder_70) -> Any -> Any
forall a b. a -> b
coe
T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> Any
forall a b. a -> b
coe T_Preorder_132
v0))
(Any -> Any
forall a b. a -> b
coe Any
v1))))
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v1 Any
v2 -> (T_Σ_14 -> T_Σ_14) -> Any
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386))
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 ->
((Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_zip_218
((T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v1
Any
v2 Any
v3)
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 Any
v5 Any
v6 Any
v7 ->
(T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsPreorder_70 -> Any -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
(T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> T_Preorder_132
forall a b. a -> b
coe T_Preorder_132
v0)) Any
v3
Any
v2 Any
v1 Any
v7 Any
v6)))))