{-# 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.Bool.Properties
import qualified MAlonzo.Code.Data.Empty
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
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- 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.Empty.T_'8869'_4) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8777''8658''8802'_8 :: T_Char_6
-> T_Char_6
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'8777''8658''8802'_8 = T_Char_6
-> T_Char_6
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
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.T_Dec_32
d__'8799'__14 :: T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8799'__14 T_Char_6
v0 T_Char_6
v1
  = ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
      (Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
      Any
forall a. a
erased
      ((Integer -> Integer -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8799'__1528
         ((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_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_250
-- Data.Char.Properties.decSetoid
d_decSetoid_22 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_22 :: T_DecSetoid_84
d_decSetoid_22
  = ((Any -> Any -> T_Dec_32) -> T_DecSetoid_84)
-> 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
      ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8799'__14)
-- Data.Char.Properties.isDecEquivalence
d_isDecEquivalence_24 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_24 :: T_IsDecEquivalence_44
d_isDecEquivalence_24
  = ((Any -> Any -> T_Dec_32) -> T_IsDecEquivalence_44)
-> Any -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isDecEquivalence_244
      ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
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_32 -> Bool) -> Any -> Bool
forall a b. a -> b
coe
      T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_16
      ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
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.T_Dec_32
d__'60''63'__44 :: T_Char_6 -> T_Char_6 -> T_Dec_32
d__'60''63'__44
  = ((Any -> Any)
 -> (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Dec_32)
-> Any -> Any -> T_Char_6 -> T_Char_6 -> T_Dec_32
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Dec_32
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_32) -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912)
-- 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_136
d_'60''45'cmp_46 :: T_Char_6 -> T_Char_6 -> T_Tri_136
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_136
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) -> T_Dec_32 -> T_Dec_32) -> Any -> Any -> t
forall a b. a -> b
coe
                    (Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    Any
forall a. a
erased
                    ((Bool -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
                       Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
                       ((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
            (let v5 :: T_Dec_32
v5
                   = Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
                       ((Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe
                          Integer -> Integer -> Bool
ltInt ((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_32
forall a b. a -> b
coe Any
forall a. a
v4 of
                  MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
v7
                    -> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
                         then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v7 of
                                MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v8
                                  -> (Any -> T_Tri_136) -> Any -> Any
forall a b. a -> b
coe Any -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 Any
v8
                                T_Reflects_14
_ -> 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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v7)
                                (case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v5 of
                                   MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
                                     -> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
                                          then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                 Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v9)
                                                 ((Any -> T_Tri_136) -> Any -> Any
forall a b. a -> b
coe
                                                    Any -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                                                    ((Integer -> T__'8804'__18) -> Any -> Any
forall a b. a -> b
coe
                                                       Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''7495''8658''60'_1566
                                                       (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 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v9)
                                                 ((Any -> T_Tri_136) -> Any -> Any
forall a b. a -> b
coe
                                                    Any -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                                                    ((Integer -> T__'8804'__18 -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                       Integer -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8804''8743''8802''8658''60'_1800
                                                       (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2)
                                                       ((Integer -> Integer -> T__'8804'__18) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          Integer -> Integer -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'8814''8658''8805'_1784
                                                          (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_32
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                  T_Dec_32
_ -> 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'__18 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''45'irrefl_86 :: T_Char_6
-> T_Char_6 -> T__'8801'__12 -> T__'8804'__18 -> T_'8869'_4
d_'60''45'irrefl_86 = T_Char_6
-> T_Char_6 -> T__'8801'__12 -> T__'8804'__18 -> T_'8869'_4
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'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_'60''45'trans_88 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
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'__18
-> T__'8804'__18
-> T__'8804'__18
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'__18 -> T__'8804'__18 -> T__'8804'__18)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
           Integer -> T__'8804'__18 -> T__'8804'__18 -> T__'8804'__18
MAlonzo.Code.Data.Nat.Properties.du_'60''45'trans_1862 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'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''45'asym_96 :: T_Char_6
-> T_Char_6 -> T__'8804'__18 -> T__'8804'__18 -> T_'8869'_4
d_'60''45'asym_96 = T_Char_6
-> T_Char_6 -> T__'8804'__18 -> T__'8804'__18 -> T_'8869'_4
forall a. a
erased
-- Data.Char.Properties.<-isStrictPartialOrder
d_'60''45'isStrictPartialOrder_102 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_102 :: T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_102
  = (T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_266)
-> Any
-> (T_Char_6
    -> T_Char_6
    -> T_Char_6
    -> T__'8804'__18
    -> T__'8804'__18
    -> T__'8804'__18)
-> Any
-> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_13145
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
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_502
d_'60''45'isStrictTotalOrder_118 :: T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder_118
  = (T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> (Any -> Any -> T_Tri_136)
 -> T_IsStrictTotalOrder_502)
-> Any -> Any -> Any -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> T_Tri_136)
-> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_23999
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      ((T_Char_6
 -> T_Char_6
 -> T_Char_6
 -> T__'8804'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any
forall a b. a -> b
coe T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
d_'60''45'trans_88) ((T_Char_6 -> T_Char_6 -> T_Tri_136) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Tri_136
d_'60''45'cmp_46)
-- Data.Char.Properties.<-strictPartialOrder
d_'60''45'strictPartialOrder_126 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_126 :: T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_126
  = (T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472)
-> T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_8957
      T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_102
-- Data.Char.Properties.<-strictTotalOrder
d_'60''45'strictTotalOrder_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_'60''45'strictTotalOrder_128 :: T_StrictTotalOrder_864
d_'60''45'strictTotalOrder_128
  = (T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864)
-> T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_16739
      T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder_118
-- Data.Char.Properties._≤?_
d__'8804''63'__130 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8804''63'__130 :: T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8804''63'__130
  = ((Any -> Any -> T_Tri_136) -> Any -> Any -> T_Dec_32)
-> Any -> T_Char_6 -> T_Char_6 -> T_Dec_32
forall a b. a -> b
coe
      (Any -> Any -> T_Tri_136) -> Any -> Any -> T_Dec_32
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties.du_decidable_184
      ((T_Char_6 -> T_Char_6 -> T_Tri_136) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Tri_136
d_'60''45'cmp_46)
-- Data.Char.Properties.≤-reflexive
d_'8804''45'reflexive_132 ::
  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_132 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T_ReflClosure_30
d_'8804''45'reflexive_132 ~T_Char_6
v0 ~T_Char_6
v1 = T__'8801'__12 -> T_ReflClosure_30
du_'8804''45'reflexive_132
du_'8804''45'reflexive_132 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'8804''45'reflexive_132 :: T__'8801'__12 -> T_ReflClosure_30
du_'8804''45'reflexive_132 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_134 ::
  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_134 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
d_'8804''45'trans_134 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'__18
 -> T__'8804'__18
 -> T__'8804'__18)
-> Any
forall a b. a -> b
coe T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8804'__18
-> T__'8804'__18
-> T__'8804'__18
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_142 ::
  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_142 :: T_Char_6
-> T_Char_6
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T__'8801'__12
d_'8804''45'antisym_142 = 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_144 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''45'isPreorder_144 :: T_IsPreorder_70
d_'8804''45'isPreorder_144
  = (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_3993
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
      (\ 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_132)
      ((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_134)
-- Data.Char.Properties.≤-isPartialOrder
d_'8804''45'isPartialOrder_146 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8804''45'isPartialOrder_146 :: T_IsPartialOrder_162
d_'8804''45'isPartialOrder_146
  = (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_144) Any
forall a. a
erased
-- Data.Char.Properties.≤-isDecPartialOrder
d_'8804''45'isDecPartialOrder_148 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_'8804''45'isDecPartialOrder_148 :: T_IsDecPartialOrder_206
d_'8804''45'isDecPartialOrder_148
  = (T_IsPartialOrder_162
 -> (Any -> Any -> T_Dec_32)
 -> (Any -> Any -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> Any -> Any -> Any -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (Any -> Any -> T_Dec_32)
-> (Any -> Any -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      (T_IsPartialOrder_162 -> Any
forall a b. a -> b
coe T_IsPartialOrder_162
d_'8804''45'isPartialOrder_146) ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8799'__14)
      ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8804''63'__130)
-- Data.Char.Properties.≤-preorder
d_'8804''45'preorder_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8804''45'preorder_150 :: T_Preorder_132
d_'8804''45'preorder_150
  = (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_2269
      T_IsPreorder_70
d_'8804''45'isPreorder_144
-- Data.Char.Properties.≤-poset
d_'8804''45'poset_152 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8804''45'poset_152 :: T_Poset_282
d_'8804''45'poset_152
  = (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_146
-- Data.Char.Properties.≤-decPoset
d_'8804''45'decPoset_154 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
d_'8804''45'decPoset_154 :: T_DecPoset_360
d_'8804''45'decPoset_154
  = (T_IsDecPartialOrder_206 -> T_DecPoset_360)
-> T_IsDecPartialOrder_206 -> T_DecPoset_360
forall a b. a -> b
coe
      T_IsDecPartialOrder_206 -> T_DecPoset_360
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_6777
      T_IsDecPartialOrder_206
d_'8804''45'isDecPartialOrder_148
-- Data.Char.Properties.toNat-injective
d_toNat'45'injective_156 ::
  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_toNat'45'injective_156 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
d_toNat'45'injective_156 = T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Char.Properties.strictTotalOrder
d_strictTotalOrder_158 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_strictTotalOrder_158 :: T_StrictTotalOrder_864
d_strictTotalOrder_158
  = (T_StrictTotalOrder_864 -> (Any -> Any) -> T_StrictTotalOrder_864)
-> Any -> Any -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_StrictTotalOrder_864 -> (Any -> Any) -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Construct.On.du_strictTotalOrder_618
      (T_StrictTotalOrder_864 -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_864
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictTotalOrder_1934)
      ((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._≈?_
d__'8776''63'__160 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8776''63'__160 :: T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8776''63'__160 T_Char_6
v0 T_Char_6
v1
  = (Integer -> Integer -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
      Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8799'__1528
      ((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.≈-refl
d_'8776''45'refl_166 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'refl_166 :: T_Char_6 -> T__'8801'__12
d_'8776''45'refl_166 = T_Char_6 -> T__'8801'__12
forall a. a
erased
-- Data.Char.Properties.≈-sym
d_'8776''45'sym_168 ::
  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_168 :: T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'sym_168 = T_Char_6 -> T_Char_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Char.Properties.≈-trans
d_'8776''45'trans_170 ::
  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_170 :: T_Char_6
-> T_Char_6
-> T_Char_6
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8776''45'trans_170 = 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_174 ::
  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_174 :: T_Level_18
-> (T_Char_6 -> T_Level_18)
-> T_Char_6
-> T_Char_6
-> T__'8801'__12
-> Any
-> Any
d_'8776''45'subst_174 ~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_174 Any
v5
du_'8776''45'subst_174 :: AgdaAny -> AgdaAny
du_'8776''45'subst_174 :: Any -> Any
du_'8776''45'subst_174 Any
v0 = Any -> Any
forall a b. a -> b
coe Any
v0
-- Data.Char.Properties.≈-isEquivalence
d_'8776''45'isEquivalence_182 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8776''45'isEquivalence_182 :: T_IsEquivalence_26
d_'8776''45'isEquivalence_182
  = ((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_743
      Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased
-- Data.Char.Properties.≈-setoid
d_'8776''45'setoid_196 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8776''45'setoid_196 :: T_Setoid_44
d_'8776''45'setoid_196
  = (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_727
      T_IsEquivalence_26
d_'8776''45'isEquivalence_182
-- Data.Char.Properties.≈-isDecEquivalence
d_'8776''45'isDecEquivalence_198 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_198 :: T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_198
  = (T_IsEquivalence_26
 -> (Any -> Any -> T_Dec_32) -> T_IsDecEquivalence_44)
-> Any -> Any -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe T_IsEquivalence_26
d_'8776''45'isEquivalence_182) ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
d__'8776''63'__160)
-- Data.Char.Properties.≈-decSetoid
d_'8776''45'decSetoid_200 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8776''45'decSetoid_200 :: T_DecSetoid_84
d_'8776''45'decSetoid_200
  = (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_1385
      T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_198
-- Data.Char.Properties.≡-setoid
d_'8801''45'setoid_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_202 :: T_Setoid_44
d_'8801''45'setoid_202 = T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe T_Setoid_44
d_setoid_20
-- Data.Char.Properties.≡-decSetoid
d_'8801''45'decSetoid_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_204 :: T_DecSetoid_84
d_'8801''45'decSetoid_204 = T_DecSetoid_84 -> T_DecSetoid_84
forall a b. a -> b
coe T_DecSetoid_84
d_decSetoid_22
-- Data.Char.Properties.<-isStrictPartialOrder-≈
d_'60''45'isStrictPartialOrder'45''8776'_206 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder'45''8776'_206 :: T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder'45''8776'_206
  = ((Any -> Any)
 -> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> Any -> Any -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
      (Any -> Any)
-> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictPartialOrder_356
      ((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_266 -> Any
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictPartialOrder_1928)
-- Data.Char.Properties.<-isStrictTotalOrder-≈
d_'60''45'isStrictTotalOrder'45''8776'_208 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder'45''8776'_208 :: T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder'45''8776'_208
  = ((Any -> Any)
 -> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502)
-> Any -> Any -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
      (Any -> Any)
-> T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Construct.On.du_isStrictTotalOrder_500
      ((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_502 -> Any
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502
MAlonzo.Code.Data.Nat.Properties.d_'60''45'isStrictTotalOrder_1930)
-- Data.Char.Properties.<-strictPartialOrder-≈
d_'60''45'strictPartialOrder'45''8776'_210 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_'60''45'strictPartialOrder'45''8776'_210 :: T_StrictPartialOrder_472
d_'60''45'strictPartialOrder'45''8776'_210
  = (T_StrictPartialOrder_472
 -> (Any -> Any) -> T_StrictPartialOrder_472)
-> Any -> Any -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_StrictPartialOrder_472
-> (Any -> Any) -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Construct.On.du_strictPartialOrder_594
      (T_StrictPartialOrder_472 -> Any
forall a b. a -> b
coe
         T_StrictPartialOrder_472
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictPartialOrder_1932)
      ((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'_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_'60''45'strictTotalOrder'45''8776'_212 :: T_StrictTotalOrder_864
d_'60''45'strictTotalOrder'45''8776'_212
  = (T_StrictTotalOrder_864 -> (Any -> Any) -> T_StrictTotalOrder_864)
-> Any -> Any -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_StrictTotalOrder_864 -> (Any -> Any) -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Construct.On.du_strictTotalOrder_618
      (T_StrictTotalOrder_864 -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_864
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictTotalOrder_1934)
      ((T_Char_6 -> Integer) -> Any
forall a b. a -> b
coe T_Char_6 -> Integer
MAlonzo.Code.Agda.Builtin.Char.d_primCharToNat_28)