{-# 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.Untyped.Relation.Binary.Structures 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.Builtin
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.Relation.Binary.Core

-- Untyped.Relation.Binary.Structures.Equivalence
d_Equivalence_10 :: p -> ()
d_Equivalence_10 p
a0 = ()
data T_Equivalence_10
  = C_constructor_26 (Integer ->
                      MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny)
                     (Integer ->
                      MAlonzo.Code.Untyped.T__'8866'_14 ->
                      MAlonzo.Code.Untyped.T__'8866'_14 ->
                      MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny -> AgdaAny)
                     (Integer ->
                      MAlonzo.Code.Untyped.T__'8866'_14 ->
                      MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny)
-- Untyped.Relation.Binary.Structures.Equivalence.~-refl
d_'126''45'refl_20 ::
  T_Equivalence_10 ->
  Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny
d_'126''45'refl_20 :: T_Equivalence_10 -> Integer -> T__'8866'_14 -> AgdaAny
d_'126''45'refl_20 T_Equivalence_10
v0
  = case T_Equivalence_10 -> T_Equivalence_10
forall a b. a -> b
coe T_Equivalence_10
v0 of
      C_constructor_26 Integer -> T__'8866'_14 -> AgdaAny
v1 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v2 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 -> (Integer -> T__'8866'_14 -> AgdaAny)
-> Integer -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> AgdaAny
v1
      T_Equivalence_10
_ -> Integer -> T__'8866'_14 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.Equivalence.~-trans
d_'126''45'trans_22 ::
  T_Equivalence_10 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny -> AgdaAny
d_'126''45'trans_22 :: T_Equivalence_10
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'126''45'trans_22 T_Equivalence_10
v0
  = case T_Equivalence_10 -> T_Equivalence_10
forall a b. a -> b
coe T_Equivalence_10
v0 of
      C_constructor_26 Integer -> T__'8866'_14 -> AgdaAny
v1 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v2 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> T__'8866'_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v2
      T_Equivalence_10
_ -> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.Equivalence.~-sym
d_'126''45'sym_24 ::
  T_Equivalence_10 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
d_'126''45'sym_24 :: T_Equivalence_10
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
d_'126''45'sym_24 T_Equivalence_10
v0
  = case T_Equivalence_10 -> T_Equivalence_10
forall a b. a -> b
coe T_Equivalence_10
v0 of
      C_constructor_26 Integer -> T__'8866'_14 -> AgdaAny
v1 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v2 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3
      T_Equivalence_10
_ -> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible
d_TermCompatible_30 :: p -> ()
d_TermCompatible_30 p
a0 = ()
data T_TermCompatible_30
  = C_constructor_150 (Integer ->
                       MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny)
                      (Integer ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny)
                      (Integer ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny -> AgdaAny)
                      (Integer ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny)
                      (Integer ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny)
                      (Integer ->
                       Integer ->
                       [MAlonzo.Code.Untyped.T__'8866'_14] ->
                       [MAlonzo.Code.Untyped.T__'8866'_14] ->
                       MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20 ->
                       AgdaAny)
                      (Integer ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       MAlonzo.Code.Untyped.T__'8866'_14 ->
                       [MAlonzo.Code.Untyped.T__'8866'_14] ->
                       [MAlonzo.Code.Untyped.T__'8866'_14] ->
                       AgdaAny ->
                       MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20 ->
                       AgdaAny)
                      (MAlonzo.Code.RawU.T_TmCon_202 -> Integer -> AgdaAny)
                      (Integer -> MAlonzo.Code.Builtin.T_Builtin_2 -> AgdaAny)
                      (Integer -> AgdaAny)
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-var
d_compat'45'var_96 ::
  T_TermCompatible_30 ->
  Integer -> MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
d_compat'45'var_96 :: T_TermCompatible_30 -> Integer -> T_Fin_10 -> AgdaAny
d_compat'45'var_96 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> T_Fin_10 -> AgdaAny) -> Integer -> T_Fin_10 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Fin_10 -> AgdaAny
v1
      T_TermCompatible_30
_ -> Integer -> T_Fin_10 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-ƛ
d_compat'45'ƛ_104 ::
  T_TermCompatible_30 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'ƛ_104 :: T_TermCompatible_30
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'ƛ_104 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2
      T_TermCompatible_30
_ -> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-·
d_compat'45''183'_106 ::
  T_TermCompatible_30 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny -> AgdaAny
d_compat'45''183'_106 :: T_TermCompatible_30
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_compat'45''183'_106 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> T__'8866'_14
 -> T__'8866'_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3
      T_TermCompatible_30
_ -> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-force
d_compat'45'force_108 ::
  T_TermCompatible_30 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'force_108 :: T_TermCompatible_30
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'force_108 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4
      T_TermCompatible_30
_ -> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-delay
d_compat'45'delay_110 ::
  T_TermCompatible_30 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'delay_110 :: T_TermCompatible_30
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
d_compat'45'delay_110 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5
      T_TermCompatible_30
_ -> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-constr
d_compat'45'constr_120 ::
  T_TermCompatible_30 ->
  Integer ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20 -> AgdaAny
d_compat'45'constr_120 :: T_TermCompatible_30
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
d_compat'45'constr_120 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer
 -> Integer
 -> [T__'8866'_14]
 -> [T__'8866'_14]
 -> T_Pointwise_20
 -> AgdaAny)
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
forall a b. a -> b
coe Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6
      T_TermCompatible_30
_ -> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-case
d_compat'45'case_132 ::
  T_TermCompatible_30 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  AgdaAny ->
  MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20 -> AgdaAny
d_compat'45'case_132 :: T_TermCompatible_30
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
d_compat'45'case_132 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> [T__'8866'_14]
 -> [T__'8866'_14]
 -> AgdaAny
 -> T_Pointwise_20
 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
forall a b. a -> b
coe Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7
      T_TermCompatible_30
_ -> Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-con
d_compat'45'con_138 ::
  T_TermCompatible_30 ->
  MAlonzo.Code.RawU.T_TmCon_202 -> Integer -> AgdaAny
d_compat'45'con_138 :: T_TermCompatible_30 -> T_TmCon_202 -> Integer -> AgdaAny
d_compat'45'con_138 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (T_TmCon_202 -> Integer -> AgdaAny)
-> T_TmCon_202 -> Integer -> AgdaAny
forall a b. a -> b
coe T_TmCon_202 -> Integer -> AgdaAny
v8
      T_TermCompatible_30
_ -> T_TmCon_202 -> Integer -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-builtin
d_compat'45'builtin_144 ::
  T_TermCompatible_30 ->
  Integer -> MAlonzo.Code.Builtin.T_Builtin_2 -> AgdaAny
d_compat'45'builtin_144 :: T_TermCompatible_30 -> Integer -> T_Builtin_2 -> AgdaAny
d_compat'45'builtin_144 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> T_Builtin_2 -> AgdaAny)
-> Integer -> T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Builtin_2 -> AgdaAny
v9
      T_TermCompatible_30
_ -> Integer -> T_Builtin_2 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Structures.TermCompatible.compat-error
d_compat'45'error_148 :: T_TermCompatible_30 -> Integer -> AgdaAny
d_compat'45'error_148 :: T_TermCompatible_30 -> Integer -> AgdaAny
d_compat'45'error_148 T_TermCompatible_30
v0
  = case T_TermCompatible_30 -> T_TermCompatible_30
forall a b. a -> b
coe T_TermCompatible_30
v0 of
      C_constructor_150 Integer -> T_Fin_10 -> AgdaAny
v1 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v2 Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v5 Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_20
-> AgdaAny
v6 Integer
-> T__'8866'_14
-> T__'8866'_14
-> [T__'8866'_14]
-> [T__'8866'_14]
-> AgdaAny
-> T_Pointwise_20
-> AgdaAny
v7 T_TmCon_202 -> Integer -> AgdaAny
v8 Integer -> T_Builtin_2 -> AgdaAny
v9 Integer -> AgdaAny
v10 -> (Integer -> AgdaAny) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> AgdaAny
v10
      T_TermCompatible_30
_ -> Integer -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError