{-# 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.Char.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.Char
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
import qualified MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties
import qualified MAlonzo.Code.Relation.Binary.Construct.On
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_'8776''8658''8801'_6 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''8658''8801'_6 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''8658''8801'_6 = T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8777''8658''8802'_8 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8777''8658''8802'_8 :: T_Char_6
-> T_Char_6
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8801'__12
-> T_Irrelevant_20
d_'8777''8658''8802'_8 = T_Char_6
-> T_Char_6
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T__'8801'__12
-> T_Irrelevant_20
forall a. a
erased
d_'8776''45'reflexive_12 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'reflexive_12 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'reflexive_12 = T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d__'8799'__14 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__14 :: T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8799'__14 T_Char_6
v0 T_Char_6
v1
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
Any
forall a. a
erased Any
forall a. a
erased
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0)
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1))
d_setoid_20 :: MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_20 :: T_Setoid_44
d_setoid_20
= T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
d_decSetoid_22 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_22 :: T_DecSetoid_84
d_decSetoid_22
= ((Any -> Any -> T_Dec_20) -> T_DecSetoid_84)
-> Any -> T_DecSetoid_84
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8799'__14)
d_isDecEquivalence_24 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_24 :: T_IsDecEquivalence_44
d_isDecEquivalence_24
= ((Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_44)
-> Any -> T_IsDecEquivalence_44
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isDecEquivalence_398
((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8799'__14)
d__'61''61'__26 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Bool
d__'61''61'__26 :: T_Char_6 -> T_Char_6 -> Bool
d__'61''61'__26 T_Char_6
v0 T_Char_6
v1
= (T_Dec_20 -> Bool) -> Any -> Bool
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_122
((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8799'__14 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v0) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1))
d__'60''63'__44 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'60''63'__44 :: T_Char_6 -> T_Char_6 -> T_Dec_20
d__'60''63'__44
= ((Any -> Any)
-> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20)
-> Any -> Any -> T_Char_6 -> T_Char_6 -> T_Dec_20
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20
MAlonzo.Code.Relation.Binary.Construct.On.du_decidable_102
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
((Integer -> Integer -> T_Dec_20) -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__3030)
d_'60''45'cmp_46 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_'60''45'cmp_46 :: T_Char_6 -> T_Char_6 -> T_Tri_158
d_'60''45'cmp_46 T_Char_6
v0 T_Char_6
v1
= let v2 :: t
v2
= (T_Char_6 -> Integer) -> T_Char_6 -> t
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0 in
Any -> T_Tri_158
forall a b. a -> b
coe
(let v3 :: t
v3
= (T_Char_6 -> Integer) -> T_Char_6 -> t
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1 in
Any -> Any
forall a b. a -> b
coe
(let v4 :: t
v4
= ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> (Any -> Any) -> Any -> t
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
Any
forall a. a
erased
(\ Any
v4 ->
(Integer -> Any) -> Any -> Any
forall a b. a -> b
coe
Integer -> Any
MAlonzo.Code.Data.Nat.Properties.du_'8801''8658''8801''7495'_2678
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0))
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
eqInt ((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0)
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1))
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
eqInt ((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0)
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1)))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v7
-> (Any -> T_Tri_158) -> Any -> Any
forall a b. a -> b
coe Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 Any
v7
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v6)
(let v7 :: Bool
v7
= Integer -> Integer -> Bool
ltInt
((T_Char_6 -> Integer) -> T_Char_6 -> Integer
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0)
((T_Char_6 -> Integer) -> T_Char_6 -> Integer
forall a b. a -> b
coe
T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1) in
Any -> Any
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v7
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
(Bool -> Any
forall a b. a -> b
coe Bool
v7))
((Any -> T_Tri_158) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172
((Integer -> T__'8804'__22) -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''7495''8658''60'_2716
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2)))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
(Bool -> Any
forall a b. a -> b
coe Bool
v7))
((Any -> T_Tri_158) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188
((Integer -> T__'8804'__22 -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''8743''8802''8658''60'_2918
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2)
((Integer -> Integer -> T__'8804'__22) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8814''8658''8805'_2902
(Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2) (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v3))))))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
d_'60''45'irrefl_86 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'irrefl_86 :: T_Char_6
-> T_Char_6 -> T__'8801'__12 -> T__'8804'__22 -> T_Irrelevant_20
d_'60''45'irrefl_86 = T_Char_6
-> T_Char_6 -> T__'8801'__12 -> T__'8804'__22 -> T_Irrelevant_20
forall a. a
erased
d_'60''45'trans_88 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'60''45'trans_88 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'60''45'trans_88 T_Char_6
v0 T_Char_6
v1 T_Char_6
v2
= ((Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
forall a b. a -> b
coe
(Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
MAlonzo.Code.Relation.Binary.Construct.On.du_transitive_64
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
(\ Any
v3 Any
v4 Any
v5 Any
v6 Any
v7 ->
(Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_2980 Any
v4 Any
v6 Any
v7)
(T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v0) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v2)
d_'60''45'asym_96 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'asym_96 :: T_Char_6
-> T_Char_6 -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20
d_'60''45'asym_96 = T_Char_6
-> T_Char_6 -> T__'8804'__22 -> T__'8804'__22 -> T_Irrelevant_20
forall a. a
erased
d_'60''45'isStrictPartialOrder_102 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_102 :: T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_102
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_290)
-> Any
-> (T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any
-> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'60''45'trans_88
((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
((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4)) ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4)))
d_'60''45'isStrictTotalOrder_118 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_118 :: T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_118
= (T_IsStrictPartialOrder_290
-> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_534)
-> Any -> Any -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
T_IsStrictPartialOrder_290
-> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
(T_IsStrictPartialOrder_290 -> Any
forall a b. a -> b
coe T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_102) ((T_Char_6 -> T_Char_6 -> T_Tri_158) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Tri_158
d_'60''45'cmp_46)
d_'60''45'strictPartialOrder_120 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_120 :: T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_120
= (T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556)
-> T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
forall a b. a -> b
coe
T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_102
d_'60''45'strictTotalOrder_122 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_122 :: T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_122
= (T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036)
-> T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_21059
T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_118
d__'8804''63'__124 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8804''63'__124 :: T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8804''63'__124
= ((Any -> Any -> T_Tri_158) -> Any -> Any -> T_Dec_20)
-> Any -> T_Char_6 -> T_Char_6 -> T_Dec_20
forall a b. a -> b
coe
(Any -> Any -> T_Tri_158) -> Any -> Any -> T_Dec_20
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties.du_decidable_184
((T_Char_6 -> T_Char_6 -> T_Tri_158) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Tri_158
d_'60''45'cmp_46)
d_'8804''45'reflexive_126 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'8804''45'reflexive_126 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T_ReflClosure_30
d_'8804''45'reflexive_126 ~T_Char_6
v0 ~T_Char_6
v1 = T__'8801'__12 -> T_ReflClosure_30
du_'8804''45'reflexive_126
du_'8804''45'reflexive_126 ::
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'8804''45'reflexive_126 :: T__'8801'__12 -> T_ReflClosure_30
du_'8804''45'reflexive_126 T__'8801'__12
v0
= T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.du_reflexive_72
d_'8804''45'trans_128 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'8804''45'trans_128 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
d_'8804''45'trans_128 T_Char_6
v0 T_Char_6
v1 T_Char_6
v2
= ((Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30)
-> Any
-> Any
-> Any
-> Any
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties.du_trans_94
((T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22)
-> Any
forall a b. a -> b
coe T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__22
-> T__'8804'__22
-> T__'8804'__22
d_'60''45'trans_88) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v0) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v2)
d_'8804''45'antisym_136 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''45'antisym_136 :: T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T__'8801'__12
d_'8804''45'antisym_136 = T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T__'8801'__12
forall a. a
erased
d_'8804''45'isPreorder_138 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''45'isPreorder_138 :: T_IsPreorder_70
d_'8804''45'isPreorder_138
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70)
-> Any -> (Any -> 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_4003
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
(\ Any
v0 Any
v1 -> (T__'8801'__12 -> T_ReflClosure_30) -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_ReflClosure_30
du_'8804''45'reflexive_126)
((T_Char_6
-> T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30)
-> Any
forall a b. a -> b
coe T_Char_6
-> T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
d_'8804''45'trans_128)
d_'8804''45'isPartialOrder_140 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8804''45'isPartialOrder_140 :: T_IsPartialOrder_174
d_'8804''45'isPartialOrder_140
= (T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174)
-> Any -> Any -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8804''45'isPreorder_138) Any
forall a. a
erased
d_'8804''45'isDecPartialOrder_142 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder_142 :: T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder_142
= (T_IsPartialOrder_174
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecPartialOrder_224)
-> Any -> Any -> Any -> T_IsDecPartialOrder_224
forall a b. a -> b
coe
T_IsPartialOrder_174
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecPartialOrder_224
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_11683
(T_IsPartialOrder_174 -> Any
forall a b. a -> b
coe T_IsPartialOrder_174
d_'8804''45'isPartialOrder_140) ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8799'__14)
((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8804''63'__124)
d_'8804''45'preorder_144 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8804''45'preorder_144 :: T_Preorder_132
d_'8804''45'preorder_144
= (T_IsPreorder_70 -> T_Preorder_132)
-> T_IsPreorder_70 -> T_Preorder_132
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
T_IsPreorder_70
d_'8804''45'isPreorder_138
d_'8804''45'poset_146 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8804''45'poset_146 :: T_Poset_314
d_'8804''45'poset_146
= (T_IsPartialOrder_174 -> T_Poset_314)
-> T_IsPartialOrder_174 -> T_Poset_314
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
T_IsPartialOrder_174
d_'8804''45'isPartialOrder_140
d_'8804''45'decPoset_148 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_406
d_'8804''45'decPoset_148 :: T_DecPoset_406
d_'8804''45'decPoset_148
= (T_IsDecPartialOrder_224 -> T_DecPoset_406)
-> T_IsDecPartialOrder_224 -> T_DecPoset_406
forall a b. a -> b
coe
T_IsDecPartialOrder_224 -> T_DecPoset_406
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_8213
T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder_142
d_'8776''45'refl_150 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'refl_150 :: T_Char_6 -> T__'8801'__12
d_'8776''45'refl_150 = T_Char_6 -> T__'8801'__12
forall a. a
erased
d_'8776''45'sym_152 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'sym_152 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'sym_152 = T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8776''45'trans_154 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_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_'8776''45'trans_154 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8776''45'trans_154 = T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'8776''45'subst_158 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> AgdaAny
d_'8776''45'subst_158 :: T_Level_18
-> (T_Char_6 -> T_Level_18)
-> T_Char_6
-> T_Char_6
-> T__'8801'__12
-> Any
-> Any
d_'8776''45'subst_158 ~T_Level_18
v0 ~T_Char_6 -> T_Level_18
v1 ~T_Char_6
v2 ~T_Char_6
v3 ~T__'8801'__12
v4 Any
v5
= Any -> Any
du_'8776''45'subst_158 Any
v5
du_'8776''45'subst_158 :: AgdaAny -> AgdaAny
du_'8776''45'subst_158 :: Any -> Any
du_'8776''45'subst_158 Any
v0 = Any -> Any
forall a b. a -> b
coe Any
v0
d__'8776''63'__166 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8776''63'__166 :: T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8776''63'__166 T_Char_6
v0 T_Char_6
v1
= (Integer -> Integer -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v0)
((T_Char_6 -> Integer) -> T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28 T_Char_6
v1)
d_'8776''45'isEquivalence_172 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8776''45'isEquivalence_172 :: T_IsEquivalence_26
d_'8776''45'isEquivalence_172
= ((Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_26)
-> Any -> Any -> Any -> T_IsEquivalence_26
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_745
Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased
d_'8776''45'setoid_174 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8776''45'setoid_174 :: T_Setoid_44
d_'8776''45'setoid_174
= (T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> T_Setoid_44
forall a b. a -> b
coe
T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
T_IsEquivalence_26
d_'8776''45'isEquivalence_172
d_'8776''45'isDecEquivalence_176 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_176 :: T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_176
= (T_IsEquivalence_26
-> (Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_44)
-> Any -> Any -> T_IsDecEquivalence_44
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe T_IsEquivalence_26
d_'8776''45'isEquivalence_172) ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
d__'8776''63'__166)
d_'8776''45'decSetoid_178 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8776''45'decSetoid_178 :: T_DecSetoid_84
d_'8776''45'decSetoid_178
= (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> T_IsDecEquivalence_44 -> T_DecSetoid_84
forall a b. a -> b
coe
T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_176
d_'8801''45'setoid_180 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_180 :: T_Setoid_44
d_'8801''45'setoid_180 = T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
d_setoid_20
d_'8801''45'decSetoid_182 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_182 :: T_DecSetoid_84
d_'8801''45'decSetoid_182 = T_DecSetoid_84 -> T_DecSetoid_84
forall a b. a -> b
coe T_DecSetoid_84
d_decSetoid_22
d_'60''45'isStrictPartialOrder'45''8776'_184 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder'45''8776'_184 :: T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder'45''8776'_184
= ((Any -> Any)
-> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290)
-> Any -> Any -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
(Any -> Any)
-> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictPartialOrder_372
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
(T_IsStrictPartialOrder_290 -> Any
forall a b. a -> b
coe
T_IsStrictPartialOrder_290
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictPartialOrder_3046)
d_'60''45'isStrictTotalOrder'45''8776'_186 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'45''8776'_186 :: T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'45''8776'_186
= ((Any -> Any)
-> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534)
-> Any -> Any -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
(Any -> Any)
-> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictTotalOrder_526
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
(T_IsStrictTotalOrder_534 -> Any
forall a b. a -> b
coe
T_IsStrictTotalOrder_534
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictTotalOrder_3048)
d_'60''45'strictPartialOrder'45''8776'_188 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder'45''8776'_188 :: T_StrictPartialOrder_556
d_'60''45'strictPartialOrder'45''8776'_188
= (T_StrictPartialOrder_556
-> (Any -> Any) -> T_StrictPartialOrder_556)
-> Any -> Any -> T_StrictPartialOrder_556
forall a b. a -> b
coe
T_StrictPartialOrder_556
-> (Any -> Any) -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Construct.On.du_strictPartialOrder_622
(T_StrictPartialOrder_556 -> Any
forall a b. a -> b
coe
T_StrictPartialOrder_556
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictPartialOrder_3050)
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
d_'60''45'strictTotalOrder'45''8776'_190 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder'45''8776'_190 :: T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder'45''8776'_190
= (T_StrictTotalOrder_1036
-> (Any -> Any) -> T_StrictTotalOrder_1036)
-> Any -> Any -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> (Any -> Any) -> T_StrictTotalOrder_1036
MAlonzo.Code.Relation.Binary.Construct.On.du_strictTotalOrder_646
(T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictTotalOrder_3052)
((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)