{-# 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.Relation.Nullary.Reflects 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core

-- Relation.Nullary.Reflects.Reflects
d_Reflects_16 :: p -> p -> p -> ()
d_Reflects_16 p
a0 p
a1 p
a2 = ()
data T_Reflects_16 = C_of'696'_22 AgdaAny | C_of'8319'_26
-- Relation.Nullary.Reflects.of
d_of_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Bool -> AgdaAny -> T_Reflects_16
d_of_30 :: () -> () -> Bool -> AgdaAny -> T_Reflects_16
d_of_30 ~()
v0 ~()
v1 Bool
v2 AgdaAny
v3 = Bool -> AgdaAny -> T_Reflects_16
du_of_30 Bool
v2 AgdaAny
v3
du_of_30 :: Bool -> AgdaAny -> T_Reflects_16
du_of_30 :: Bool -> AgdaAny -> T_Reflects_16
du_of_30 Bool
v0 AgdaAny
v1
  = if Bool -> Bool
forall a b. a -> b
coe Bool
v0 then (AgdaAny -> T_Reflects_16) -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) else T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
C_of'8319'_26
-- Relation.Nullary.Reflects.invert
d_invert_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Bool -> T_Reflects_16 -> AgdaAny
d_invert_38 :: () -> () -> Bool -> T_Reflects_16 -> AgdaAny
d_invert_38 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 = T_Reflects_16 -> AgdaAny
du_invert_38 T_Reflects_16
v3
du_invert_38 :: T_Reflects_16 -> AgdaAny
du_invert_38 :: T_Reflects_16 -> AgdaAny
du_invert_38 T_Reflects_16
v0
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
      C_of'696'_22 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Reflects_16
C_of'8319'_26 -> AgdaAny
forall a. a
erased
      T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects.recompute
d_recompute_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Bool -> T_Reflects_16 -> AgdaAny -> AgdaAny
d_recompute_46 :: () -> () -> Bool -> T_Reflects_16 -> AgdaAny -> AgdaAny
d_recompute_46 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 ~AgdaAny
v4 = T_Reflects_16 -> AgdaAny
du_recompute_46 T_Reflects_16
v3
du_recompute_46 :: T_Reflects_16 -> AgdaAny
du_recompute_46 :: T_Reflects_16 -> AgdaAny
du_recompute_46 T_Reflects_16
v0
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
      C_of'696'_22 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Reflects_16
C_of'8319'_26
        -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction'45'irr_38
      T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects.recompute-constant
d_recompute'45'constant_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  T_Reflects_16 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_recompute'45'constant_62 :: ()
-> ()
-> Bool
-> T_Reflects_16
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_recompute'45'constant_62 = ()
-> ()
-> Bool
-> T_Reflects_16
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Reflects.T-reflects
d_T'45'reflects_66 :: Bool -> T_Reflects_16
d_T'45'reflects_66 :: Bool -> T_Reflects_16
d_T'45'reflects_66 Bool
v0
  = if Bool -> Bool
forall a b. a -> b
coe Bool
v0
      then (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      else (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Relation.Nullary.Reflects.¬-reflects
d_'172''45'reflects_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Bool -> T_Reflects_16 -> T_Reflects_16
d_'172''45'reflects_70 :: () -> () -> Bool -> T_Reflects_16 -> T_Reflects_16
d_'172''45'reflects_70 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 = T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 T_Reflects_16
v3
du_'172''45'reflects_70 :: T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 :: T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 T_Reflects_16
v0
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
      C_of'696'_22 AgdaAny
v1
        -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30
             ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v1))
      T_Reflects_16
C_of'8319'_26
        -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30
             ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
             AgdaAny
forall a. a
erased
      T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects._×-reflects_
d__'215''45'reflects__82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'215''45'reflects__82 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'215''45'reflects__82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
  = Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'215''45'reflects__82 ::
  Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
      C_of'696'_22 AgdaAny
v3
        -> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
             C_of'696'_22 AgdaAny
v4
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
                    ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             T_Reflects_16
C_of'8319'_26
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                    AgdaAny
forall a. a
erased
             T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Reflects_16
C_of'8319'_26
        -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30
             ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
             AgdaAny
forall a. a
erased
      T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects._⊎-reflects_
d__'8846''45'reflects__98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'8846''45'reflects__98 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'8846''45'reflects__98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
  = Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'8846''45'reflects__98 ::
  Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
      C_of'696'_22 AgdaAny
v3
        -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30
             ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10) (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
             ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
      T_Reflects_16
C_of'8319'_26
        -> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
             C_of'696'_22 AgdaAny
v4
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
                    ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             T_Reflects_16
C_of'8319'_26
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                    AgdaAny
forall a. a
erased
             T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects._→-reflects_
d__'8594''45'reflects__114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'8594''45'reflects__114 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'8594''45'reflects__114 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
  = Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'8594''45'reflects__114 ::
  Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
  = case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
      C_of'696'_22 AgdaAny
v3
        -> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
             C_of'696'_22 AgdaAny
v4
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                       ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
                          (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
v4))
             T_Reflects_16
C_of'8319'_26
               -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
                    Bool -> AgdaAny -> T_Reflects_16
du_of_30
                    ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                       ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
                          (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
                       (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                    AgdaAny
forall a. a
erased
             T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Reflects_16
C_of'8319'_26
        -> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30
             ((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
                ((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
                   (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                     AgdaAny
forall a. a
erased))
      T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects.fromEquivalence
d_fromEquivalence_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
d_fromEquivalence_132 :: ()
-> ()
-> Bool
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Reflects_16
d_fromEquivalence_132 ~()
v0 ~()
v1 Bool
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
  = Bool
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 Bool
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
du_fromEquivalence_132 ::
  Bool ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 :: Bool
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 Bool
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = if Bool -> Bool
forall a b. a -> b
coe Bool
v0
      then (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
             Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
             ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      else (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
-- Relation.Nullary.Reflects.det
d_det_146 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  Bool ->
  T_Reflects_16 ->
  T_Reflects_16 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_det_146 :: ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T__'8801'__12
d_det_146 = ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Reflects.T-reflects-elim
d_T'45'reflects'45'elim_164 ::
  Bool ->
  Bool ->
  T_Reflects_16 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_T'45'reflects'45'elim_164 :: Bool -> Bool -> T_Reflects_16 -> T__'8801'__12
d_T'45'reflects'45'elim_164 = Bool -> Bool -> T_Reflects_16 -> T__'8801'__12
forall a. a
erased