{-# 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.Reasoning.Setoid 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.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Reasoning.Base.Single
import qualified MAlonzo.Code.Relation.Binary.Structures
d__IsRelatedTo__38 :: p -> p -> p -> p -> p -> ()
d__IsRelatedTo__38 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d__'8718'_40 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d__'8718'_40 :: () -> () -> T_Setoid_44 -> AgdaAny -> T__IsRelatedTo__26
d__'8718'_40 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44 -> AgdaAny -> T__IsRelatedTo__26
du__'8718'_40 T_Setoid_44
v2
du__'8718'_40 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
du__'8718'_40 :: T_Setoid_44 -> AgdaAny -> T__IsRelatedTo__26
du__'8718'_40 T_Setoid_44
v0
= ((AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__26
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> AgdaAny -> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du__'8718'_86
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
d__'8801''10216''10217'__42 ::
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d__'8801''10216''10217'__42 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
d__'8801''10216''10217'__42 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
d_begin__44 ::
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
AgdaAny
d_begin__44 :: T__IsRelatedTo__26 -> AgdaAny
d_begin__44
= (T__IsRelatedTo__26 -> AgdaAny) -> T__IsRelatedTo__26 -> AgdaAny
forall a b. a -> b
coe
T__IsRelatedTo__26 -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.d_begin__40
d_step'45''8801'_50 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d_step'45''8801'_50 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__'8801'__12
-> T__IsRelatedTo__26
d_step'45''8801'_50 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~AgdaAny
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__IsRelatedTo__26
v6 ~T__'8801'__12
v7
= T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801'_50 T__IsRelatedTo__26
v6
du_step'45''8801'_50 ::
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
du_step'45''8801'_50 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801'_50 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
d_step'45''8801''728'_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d_step'45''8801''728'_52 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> T__'8801'__12
-> T__IsRelatedTo__26
d_step'45''8801''728'_52 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~AgdaAny
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__IsRelatedTo__26
v6 ~T__'8801'__12
v7
= T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801''728'_52 T__IsRelatedTo__26
v6
du_step'45''8801''728'_52 ::
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
du_step'45''8801''728'_52 :: T__IsRelatedTo__26 -> T__IsRelatedTo__26
du_step'45''8801''728'_52 T__IsRelatedTo__26
v0 = T__IsRelatedTo__26 -> T__IsRelatedTo__26
forall a b. a -> b
coe T__IsRelatedTo__26
v0
d_step'45''8776'_58 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d_step'45''8776'_58 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
d_step'45''8776'_58 ~()
v0 ~()
v1 T_Setoid_44
v2 = T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8776'_58 T_Setoid_44
v2
du_step'45''8776'_58 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
du_step'45''8776'_58 :: T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8776'_58 T_Setoid_44
v0
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_step'45''8764'_50
((T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
((T_Setoid_44 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
v0)))
d_step'45''8776''728'_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
d_step'45''8776''728'_66 :: ()
-> ()
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
d_step'45''8776''728'_66 ~()
v0 ~()
v1 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__IsRelatedTo__26
v6 AgdaAny
v7
= T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8776''728'_66 T_Setoid_44
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__IsRelatedTo__26
v6 AgdaAny
v7
du_step'45''8776''728'_66 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
AgdaAny ->
MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
du_step'45''8776''728'_66 :: T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8776''728'_66 T_Setoid_44
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__26
v4 AgdaAny
v5
= (T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26)
-> T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
forall a b. a -> b
coe
T_Setoid_44
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__26
-> AgdaAny
-> T__IsRelatedTo__26
du_step'45''8776'_58 T_Setoid_44
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__26
v4
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
(T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
v0))
AgdaAny
v2 AgdaAny
v1 AgdaAny
v5)