{-# 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

-- Data.Char.Properties.≈⇒≡
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
-- Data.Char.Properties.≉⇒≢
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
-- Data.Char.Properties.≈-reflexive
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
-- Data.Char.Properties._≟_
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'_178
      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'__2796
         ((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))
-- Data.Char.Properties.setoid
d_setoid_20 :: MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_setoid_20 :: T_Setoid_46
d_setoid_20
  = T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe
      T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
-- Data.Char.Properties.decSetoid
d_decSetoid_22 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_decSetoid_22 :: T_DecSetoid_90
d_decSetoid_22
  = ((Any -> Any -> T_Dec_20) -> T_DecSetoid_90)
-> Any -> T_DecSetoid_90
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_20) -> T_DecSetoid_90
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)
-- Data.Char.Properties.isDecEquivalence
d_isDecEquivalence_24 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
d_isDecEquivalence_24 :: T_IsDecEquivalence_48
d_isDecEquivalence_24
  = ((Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_48)
-> Any -> T_IsDecEquivalence_48
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_48
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)
-- Data.Char.Properties._==_
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_132
      ((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))
-- Data.Char.Properties._<?_
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'__3172)
-- Data.Char.Properties.<-cmp
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 :: Any
v2
          = (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 in
    Any -> T_Tri_158
forall a b. a -> b
coe
      (let v3 :: Any
v3
             = (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
         (let v4 :: Any
v4
                = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> (Any -> Any) -> Any -> Any
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'_178
                    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'_2786
                         ((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_70
                          ((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
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_70
                                             (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'_2824
                                                (Any -> Any
forall a b. a -> b
coe Any
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_70
                                             (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'_3060
                                                (Any -> Any
forall a b. a -> b
coe Any
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'_3044
                                                   (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v3))))))
               T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
-- Data.Char.Properties.<-irrefl
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
-- Data.Char.Properties.<-trans
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_3122 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)
-- Data.Char.Properties.<-asym
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
-- Data.Char.Properties.<-isStrictPartialOrder
d_'60''45'isStrictPartialOrder_102 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_102 :: T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_102
  = (T_IsEquivalence_28
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> Any
-> (T_Char_6
    -> T_Char_6
    -> T_Char_6
    -> T__'8804'__22
    -> T__'8804'__22
    -> T__'8804'__22)
-> Any
-> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
      (T_IsEquivalence_28 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_28
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)))
-- Data.Char.Properties.<-isStrictTotalOrder
d_'60''45'isStrictTotalOrder_118 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder_118 :: T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder_118
  = (T_IsStrictPartialOrder_370
 -> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_624)
-> Any -> Any -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370
-> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Structures.C_constructor_680
      (T_IsStrictPartialOrder_370 -> Any
forall a b. a -> b
coe T_IsStrictPartialOrder_370
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)
-- Data.Char.Properties.<-strictPartialOrder
d_'60''45'strictPartialOrder_120 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_120 :: T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_120
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_102
-- Data.Char.Properties.<-strictTotalOrder
d_'60''45'strictTotalOrder_122 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder_122 :: T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder_122
  = (T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280)
-> T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1386
      T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder_118
-- Data.Char.Properties._≤?_
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)
-- Data.Char.Properties.≤-reflexive
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
-- Data.Char.Properties.≤-trans
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)
-- Data.Char.Properties.≤-antisym
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
-- Data.Char.Properties.≤-isPreorder
d_'8804''45'isPreorder_138 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_'8804''45'isPreorder_138 :: T_IsPreorder_76
d_'8804''45'isPreorder_138
  = (T_IsEquivalence_28
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsPreorder_76)
-> Any -> (Any -> Any -> Any) -> Any -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      (T_IsEquivalence_28 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_28
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)
-- Data.Char.Properties.≤-isPartialOrder
d_'8804''45'isPartialOrder_140 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'8804''45'isPartialOrder_140 :: T_IsPartialOrder_248
d_'8804''45'isPartialOrder_140
  = (T_IsPreorder_76
 -> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_248)
-> Any -> Any -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      (T_IsPreorder_76 -> Any
forall a b. a -> b
coe T_IsPreorder_76
d_'8804''45'isPreorder_138) Any
forall a. a
erased
-- Data.Char.Properties.≤-isDecPartialOrder
d_'8804''45'isDecPartialOrder_142 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
d_'8804''45'isDecPartialOrder_142 :: T_IsDecPartialOrder_300
d_'8804''45'isDecPartialOrder_142
  = (T_IsPartialOrder_248
 -> (Any -> Any -> T_Dec_20)
 -> (Any -> Any -> T_Dec_20)
 -> T_IsDecPartialOrder_300)
-> Any -> Any -> Any -> T_IsDecPartialOrder_300
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecPartialOrder_300
MAlonzo.Code.Relation.Binary.Structures.C_constructor_364
      (T_IsPartialOrder_248 -> Any
forall a b. a -> b
coe T_IsPartialOrder_248
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)
-- Data.Char.Properties.≤-preorder
d_'8804''45'preorder_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_'8804''45'preorder_144 :: T_Preorder_142
d_'8804''45'preorder_144
  = (T_IsPreorder_76 -> T_Preorder_142)
-> T_IsPreorder_76 -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      T_IsPreorder_76
d_'8804''45'isPreorder_138
-- Data.Char.Properties.≤-poset
d_'8804''45'poset_146 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'8804''45'poset_146 :: T_Poset_492
d_'8804''45'poset_146
  = (T_IsPartialOrder_248 -> T_Poset_492)
-> T_IsPartialOrder_248 -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      T_IsPartialOrder_248
d_'8804''45'isPartialOrder_140
-- Data.Char.Properties.≤-decPoset
d_'8804''45'decPoset_148 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_596
d_'8804''45'decPoset_148 :: T_DecPoset_596
d_'8804''45'decPoset_148
  = (T_IsDecPartialOrder_300 -> T_DecPoset_596)
-> T_IsDecPartialOrder_300 -> T_DecPoset_596
forall a b. a -> b
coe
      T_IsDecPartialOrder_300 -> T_DecPoset_596
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_752
      T_IsDecPartialOrder_300
d_'8804''45'isDecPartialOrder_142
-- Data.Char.Properties.≈-refl
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
-- Data.Char.Properties.≈-sym
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
-- Data.Char.Properties.≈-trans
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
-- Data.Char.Properties.≈-subst
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
-- Data.Char.Properties._≈?_
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'__2796
      ((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)
-- Data.Char.Properties.≈-isEquivalence
d_'8776''45'isEquivalence_172 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_'8776''45'isEquivalence_172 :: T_IsEquivalence_28
d_'8776''45'isEquivalence_172
  = ((Any -> Any)
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsEquivalence_28)
-> Any -> Any -> Any -> T_IsEquivalence_28
forall a b. a -> b
coe
      (Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.C_constructor_46 Any
forall a. a
erased
      Any
forall a. a
erased Any
forall a. a
erased
-- Data.Char.Properties.≈-setoid
d_'8776''45'setoid_174 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'8776''45'setoid_174 :: T_Setoid_46
d_'8776''45'setoid_174
  = (T_IsEquivalence_28 -> T_Setoid_46)
-> T_IsEquivalence_28 -> T_Setoid_46
forall a b. a -> b
coe
      T_IsEquivalence_28 -> T_Setoid_46
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_84
      T_IsEquivalence_28
d_'8776''45'isEquivalence_172
-- Data.Char.Properties.≈-isDecEquivalence
d_'8776''45'isDecEquivalence_176 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_48
d_'8776''45'isDecEquivalence_176 :: T_IsDecEquivalence_48
d_'8776''45'isDecEquivalence_176
  = (T_IsEquivalence_28
 -> (Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_48)
-> Any -> Any -> T_IsDecEquivalence_48
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (Any -> Any -> T_Dec_20) -> T_IsDecEquivalence_48
MAlonzo.Code.Relation.Binary.Structures.C_constructor_70
      (T_IsEquivalence_28 -> Any
forall a b. a -> b
coe T_IsEquivalence_28
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)
-- Data.Char.Properties.≈-decSetoid
d_'8776''45'decSetoid_178 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_'8776''45'decSetoid_178 :: T_DecSetoid_90
d_'8776''45'decSetoid_178
  = (T_IsDecEquivalence_48 -> T_DecSetoid_90)
-> T_IsDecEquivalence_48 -> T_DecSetoid_90
forall a b. a -> b
coe
      T_IsDecEquivalence_48 -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_134
      T_IsDecEquivalence_48
d_'8776''45'isDecEquivalence_176
-- Data.Char.Properties.≡-setoid
d_'8801''45'setoid_180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46
d_'8801''45'setoid_180 :: T_Setoid_46
d_'8801''45'setoid_180 = T_Setoid_46 -> T_Setoid_46
forall a b. a -> b
coe T_Setoid_46
d_setoid_20
-- Data.Char.Properties.≡-decSetoid
d_'8801''45'decSetoid_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_90
d_'8801''45'decSetoid_182 :: T_DecSetoid_90
d_'8801''45'decSetoid_182 = T_DecSetoid_90 -> T_DecSetoid_90
forall a b. a -> b
coe T_DecSetoid_90
d_decSetoid_22
-- Data.Char.Properties.<-isStrictPartialOrder-≈
d_'60''45'isStrictPartialOrder'45''8776'_184 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder'45''8776'_184 :: T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder'45''8776'_184
  = ((Any -> Any)
 -> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> Any -> Any -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      (Any -> Any)
-> T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictPartialOrder_374
      ((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_370 -> Any
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictPartialOrder_3188)
-- Data.Char.Properties.<-isStrictTotalOrder-≈
d_'60''45'isStrictTotalOrder'45''8776'_186 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder'45''8776'_186 :: T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder'45''8776'_186
  = ((Any -> Any)
 -> T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624)
-> Any -> Any -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
      (Any -> Any)
-> T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictTotalOrder_530
      ((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_624 -> Any
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictTotalOrder_3190)
-- Data.Char.Properties.<-strictPartialOrder-≈
d_'60''45'strictPartialOrder'45''8776'_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_'60''45'strictPartialOrder'45''8776'_188 :: T_StrictPartialOrder_760
d_'60''45'strictPartialOrder'45''8776'_188
  = (T_StrictPartialOrder_760
 -> (Any -> Any) -> T_StrictPartialOrder_760)
-> Any -> Any -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_StrictPartialOrder_760
-> (Any -> Any) -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Construct.On.du_strictPartialOrder_626
      (T_StrictPartialOrder_760 -> Any
forall a b. a -> b
coe
         T_StrictPartialOrder_760
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictPartialOrder_3192)
      ((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)
-- Data.Char.Properties.<-strictTotalOrder-≈
d_'60''45'strictTotalOrder'45''8776'_190 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder'45''8776'_190 :: T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder'45''8776'_190
  = (T_StrictTotalOrder_1280
 -> (Any -> Any) -> T_StrictTotalOrder_1280)
-> Any -> Any -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_StrictTotalOrder_1280 -> (Any -> Any) -> T_StrictTotalOrder_1280
MAlonzo.Code.Relation.Binary.Construct.On.du_strictTotalOrder_650
      (T_StrictTotalOrder_1280 -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_1280
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictTotalOrder_3194)
      ((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)