{-# 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.String.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.Equality
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Char.Properties
import qualified MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.On
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Data.String.Properties.≈⇒≡
d_'8776''8658''8801'_6 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''8658''8801'_6 :: T_String_6 -> T_String_6 -> T_Pointwise_48 -> T__'8801'__12
d_'8776''8658''8801'_6 = T_String_6 -> T_String_6 -> T_Pointwise_48 -> T__'8801'__12
forall a. a
erased
-- Data.String.Properties.≈-reflexive
d_'8776''45'reflexive_8 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8776''45'reflexive_8 :: T_String_6 -> T_String_6 -> T__'8801'__12 -> T_Pointwise_48
d_'8776''45'reflexive_8 T_String_6
v0 ~T_String_6
v1 ~T__'8801'__12
v2 = T_String_6 -> T_Pointwise_48
du_'8776''45'reflexive_8 T_String_6
v0
du_'8776''45'reflexive_8 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8776''45'reflexive_8 :: T_String_6 -> T_Pointwise_48
du_'8776''45'reflexive_8 T_String_6
v0
  = ([Any] -> T_Pointwise_48) -> Any -> T_Pointwise_48
forall a b. a -> b
coe
      [Any] -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_'8801''8658'Pointwise'45''8801'_590
      ((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
-- Data.String.Properties.≈-refl
d_'8776''45'refl_10 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8776''45'refl_10 :: T_String_6 -> T_Pointwise_48
d_'8776''45'refl_10 T_String_6
v0 = (T_String_6 -> T_Pointwise_48) -> Any -> T_Pointwise_48
forall a b. a -> b
coe T_String_6 -> T_Pointwise_48
du_'8776''45'reflexive_8 (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0)
-- Data.String.Properties.≈-sym
d_'8776''45'sym_14 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8776''45'sym_14 :: T_String_6 -> T_String_6 -> T_Pointwise_48 -> T_Pointwise_48
d_'8776''45'sym_14 T_String_6
v0 T_String_6
v1
  = ((Any -> Any -> Any -> Any)
 -> [Any] -> [Any] -> T_Pointwise_48 -> T_Pointwise_48)
-> Any -> Any -> Any -> T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any)
-> [Any] -> [Any] -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_symmetric_40
      Any
forall a. a
erased
      (((Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any)
-> (T_String_6 -> String)
-> (Any -> Any -> Any)
-> T_String_6
-> T_String_6
-> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_292
         T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12
         (\ Any
v2 Any
v3 -> Any
v2) T_String_6
v0 T_String_6
v1)
      (((Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (T_String_6 -> String)
-> T_String_6
-> T_String_6
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__298
         (\ Any
v2 Any
v3 -> Any
v3)
         T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0 T_String_6
v1)
-- Data.String.Properties.≈-trans
d_'8776''45'trans_16 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8776''45'trans_16 :: T_String_6
-> T_String_6
-> T_String_6
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'8776''45'trans_16 T_String_6
v0 T_String_6
v1 T_String_6
v2
  = ((Any -> Any -> Any -> Any -> Any -> Any)
 -> [Any]
 -> [Any]
 -> [Any]
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> Any
-> Any
-> Any
-> Any
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any -> Any -> Any)
-> [Any]
-> [Any]
-> [Any]
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_transitive_50
      Any
forall a. a
erased
      (((Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any)
-> (T_String_6 -> String)
-> (Any -> Any -> Any)
-> T_String_6
-> T_String_6
-> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_292
         T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12
         (\ Any
v3 Any
v4 -> Any
v3) T_String_6
v0 T_String_6
v1)
      (((Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (T_String_6 -> String)
-> T_String_6
-> T_String_6
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__298
         (\ Any
v3 Any
v4 -> Any
v4)
         T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0 T_String_6
v1)
      (((Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (T_String_6 -> String)
-> T_String_6
-> T_String_6
-> Any
forall a b. a -> b
coe
         (Any -> Any -> Any) -> (Any -> Any) -> Any -> Any -> Any
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__298
         (\ Any
v3 Any
v4 -> Any
v4)
         T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1 T_String_6
v2)
-- Data.String.Properties.≈-subst
d_'8776''45'subst_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()) ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  AgdaAny -> AgdaAny
d_'8776''45'subst_20 :: T_Level_18
-> (T_String_6 -> T_Level_18)
-> T_String_6
-> T_String_6
-> T_Pointwise_48
-> Any
-> Any
d_'8776''45'subst_20 ~T_Level_18
v0 ~T_String_6 -> T_Level_18
v1 ~T_String_6
v2 ~T_String_6
v3 ~T_Pointwise_48
v4 Any
v5
  = Any -> Any
du_'8776''45'subst_20 Any
v5
du_'8776''45'subst_20 :: AgdaAny -> AgdaAny
du_'8776''45'subst_20 :: Any -> Any
du_'8776''45'subst_20 Any
v0 = Any -> Any
forall a b. a -> b
coe Any
v0
-- Data.String.Properties._≈?_
d__'8776''63'__28 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8776''63'__28 :: T_String_6 -> T_String_6 -> T_Dec_20
d__'8776''63'__28 T_String_6
v0 T_String_6
v1
  = ((Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
      ((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
MAlonzo.Code.Data.Char.Properties.d__'8799'__14)
      ((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
      ((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1)
-- Data.String.Properties.≈-isEquivalence
d_'8776''45'isEquivalence_34 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8776''45'isEquivalence_34 :: T_IsEquivalence_26
d_'8776''45'isEquivalence_34
  = ((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
      ((T_String_6 -> T_Pointwise_48) -> Any
forall a b. a -> b
coe T_String_6 -> T_Pointwise_48
d_'8776''45'refl_10) ((T_String_6 -> T_String_6 -> T_Pointwise_48 -> T_Pointwise_48)
-> Any
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Pointwise_48 -> T_Pointwise_48
d_'8776''45'sym_14)
      ((T_String_6
 -> T_String_6
 -> T_String_6
 -> T_Pointwise_48
 -> T_Pointwise_48
 -> T_Pointwise_48)
-> Any
forall a b. a -> b
coe T_String_6
-> T_String_6
-> T_String_6
-> T_Pointwise_48
-> T_Pointwise_48
-> T_Pointwise_48
d_'8776''45'trans_16)
-- Data.String.Properties.≈-setoid
d_'8776''45'setoid_48 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8776''45'setoid_48 :: T_Setoid_44
d_'8776''45'setoid_48
  = (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_34
-- Data.String.Properties.≈-isDecEquivalence
d_'8776''45'isDecEquivalence_50 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_50 :: T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_50
  = (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_34) ((T_String_6 -> T_String_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
d__'8776''63'__28)
-- Data.String.Properties.≈-decSetoid
d_'8776''45'decSetoid_52 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8776''45'decSetoid_52 :: T_DecSetoid_84
d_'8776''45'decSetoid_52
  = (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_50
-- Data.String.Properties._≟_
d__'8799'__54 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__54 :: T_String_6 -> T_String_6 -> T_Dec_20
d__'8799'__54 T_String_6
v0 T_String_6
v1
  = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> (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
v2 -> (T_String_6 -> T_Pointwise_48) -> Any -> Any
forall a b. a -> b
coe T_String_6 -> T_Pointwise_48
du_'8776''45'reflexive_8 (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0))
      ((T_String_6 -> T_String_6 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
d__'8776''63'__28 (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0) (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v1))
-- Data.String.Properties.≡-setoid
d_'8801''45'setoid_60 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_60 :: T_Setoid_44
d_'8801''45'setoid_60
  = T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe
      T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
-- Data.String.Properties.≡-decSetoid
d_'8801''45'decSetoid_62 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_62 :: T_DecSetoid_84
d_'8801''45'decSetoid_62
  = ((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_String_6 -> T_String_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
d__'8799'__54)
-- Data.String.Properties._<?_
d__'60''63'__64 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'60''63'__64 :: T_String_6 -> T_String_6 -> T_Dec_20
d__'60''63'__64 T_String_6
v0 T_String_6
v1
  = ((Any -> Any -> T_Dec_20)
 -> (Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> (T_Char_6 -> T_Char_6 -> T_Dec_20)
-> (T_Char_6 -> T_Char_6 -> T_Dec_20)
-> Any
-> Any
-> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'60''45'decidable_274
      T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'8799'__14
      T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'60''63'__44
      ((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
      ((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1)
-- Data.String.Properties.<-isStrictPartialOrder-≈
d_'60''45'isStrictPartialOrder'45''8776'_70 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder'45''8776'_70 :: T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder'45''8776'_70
  = ((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_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
      ((T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290)
-> Any -> Any
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'60''45'isStrictPartialOrder_278
         (T_IsStrictPartialOrder_290 -> Any
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290
MAlonzo.Code.Data.Char.Properties.d_'60''45'isStrictPartialOrder_102))
-- Data.String.Properties.<-isStrictTotalOrder-≈
d_'60''45'isStrictTotalOrder'45''8776'_72 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'45''8776'_72 :: T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder'45''8776'_72
  = ((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_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
      ((T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534)
-> Any -> Any
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'60''45'isStrictTotalOrder_314
         (T_IsStrictTotalOrder_534 -> Any
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534
MAlonzo.Code.Data.Char.Properties.d_'60''45'isStrictTotalOrder_118))
-- Data.String.Properties.<-strictPartialOrder-≈
d_'60''45'strictPartialOrder'45''8776'_74 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder'45''8776'_74 :: T_StrictPartialOrder_556
d_'60''45'strictPartialOrder'45''8776'_74
  = (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 -> T_StrictPartialOrder_556)
-> Any -> Any
forall a b. a -> b
coe
         T_StrictPartialOrder_556 -> T_StrictPartialOrder_556
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'60''45'strictPartialOrder_374
         (T_StrictPartialOrder_556 -> Any
forall a b. a -> b
coe
            T_StrictPartialOrder_556
MAlonzo.Code.Data.Char.Properties.d_'60''45'strictPartialOrder_120))
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
-- Data.String.Properties.<-strictTotalOrder-≈
d_'60''45'strictTotalOrder'45''8776'_76 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder'45''8776'_76 :: T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder'45''8776'_76
  = (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 -> T_StrictTotalOrder_1036) -> Any -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'60''45'strictTotalOrder_442
         (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe
            T_StrictTotalOrder_1036
MAlonzo.Code.Data.Char.Properties.d_'60''45'strictTotalOrder_122))
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
-- Data.String.Properties.≤-isDecPartialOrder-≈
d_'8804''45'isDecPartialOrder'45''8776'_78 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder'45''8776'_78 :: T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder'45''8776'_78
  = ((Any -> Any)
 -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224)
-> Any -> Any -> T_IsDecPartialOrder_224
forall a b. a -> b
coe
      (Any -> Any) -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224
MAlonzo.Code.Relation.Binary.Construct.On.du_isDecPartialOrder_314
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
      ((T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224) -> Any -> Any
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'8804''45'isDecPartialOrder_726
         (T_IsStrictTotalOrder_534 -> Any
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534
MAlonzo.Code.Data.Char.Properties.d_'60''45'isStrictTotalOrder_118))
-- Data.String.Properties.≤-isDecTotalOrder-≈
d_'8804''45'isDecTotalOrder'45''8776'_80 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder'45''8776'_80 :: T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder'45''8776'_80
  = ((Any -> Any) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460)
-> Any -> Any -> T_IsDecTotalOrder_460
forall a b. a -> b
coe
      (Any -> Any) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460
MAlonzo.Code.Relation.Binary.Construct.On.du_isDecTotalOrder_460
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
      ((T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460) -> Any -> Any
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'8804''45'isDecTotalOrder_834
         (T_IsStrictTotalOrder_534 -> Any
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534
MAlonzo.Code.Data.Char.Properties.d_'60''45'isStrictTotalOrder_118))
-- Data.String.Properties.≤-decTotalOrder-≈
d_'8804''45'decTotalOrder'45''8776'_82 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
d_'8804''45'decTotalOrder'45''8776'_82 :: T_DecTotalOrder_866
d_'8804''45'decTotalOrder'45''8776'_82
  = (T_DecTotalOrder_866 -> (Any -> Any) -> T_DecTotalOrder_866)
-> Any -> Any -> T_DecTotalOrder_866
forall a b. a -> b
coe
      T_DecTotalOrder_866 -> (Any -> Any) -> T_DecTotalOrder_866
MAlonzo.Code.Relation.Binary.Construct.On.du_decTotalOrder_638
      ((T_StrictTotalOrder_1036 -> T_DecTotalOrder_866) -> Any -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_1036 -> T_DecTotalOrder_866
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'8804''45'decTotalOrder_1130
         (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe
            T_StrictTotalOrder_1036
MAlonzo.Code.Data.Char.Properties.d_'60''45'strictTotalOrder_122))
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
-- Data.String.Properties.≤-decPoset-≈
d_'8804''45'decPoset'45''8776'_84 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_406
d_'8804''45'decPoset'45''8776'_84 :: T_DecPoset_406
d_'8804''45'decPoset'45''8776'_84
  = (T_DecPoset_406 -> (Any -> Any) -> T_DecPoset_406)
-> Any -> Any -> T_DecPoset_406
forall a b. a -> b
coe
      T_DecPoset_406 -> (Any -> Any) -> T_DecPoset_406
MAlonzo.Code.Relation.Binary.Construct.On.du_decPoset_614
      ((T_StrictTotalOrder_1036 -> T_DecPoset_406) -> Any -> Any
forall a b. a -> b
coe
         T_StrictTotalOrder_1036 -> T_DecPoset_406
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict.du_'8804''45'decPoset_1038
         (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe
            T_StrictTotalOrder_1036
MAlonzo.Code.Data.Char.Properties.d_'60''45'strictTotalOrder_122))
      ((T_String_6 -> String) -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12)
-- Data.String.Properties._==_
d__'61''61'__86 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d__'61''61'__86 :: T_String_6 -> T_String_6 -> Bool
d__'61''61'__86 T_String_6
v0 T_String_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_String_6 -> T_String_6 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
d__'8799'__54 (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0) (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v1))