{-# 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.Binary.Construct.Closure.Reflexive 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.Primitive

-- Relation.Binary.Construct.Closure.Reflexive.ReflClosure
d_ReflClosure_30 :: p -> p -> p -> p -> p -> p -> ()
d_ReflClosure_30 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_ReflClosure_30 = C_refl_36 | C_'91'_'93'_44 AgdaAny
-- Relation.Binary.Construct.Closure.Reflexive.map
d_map_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
d_map_52 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
d_map_52 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_map_52 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
du_map_52 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_map_52 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_map_52 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
C_refl_36 -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
C_refl_36
      C_'91'_'93'_44 AgdaAny
v6 -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe AgdaAny -> T_ReflClosure_30
C_'91'_'93'_44 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6)
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.drop-refl
d_drop'45'refl_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny
d_drop'45'refl_62 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
d_drop'45'refl_62 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 AgdaAny -> AgdaAny
v4 AgdaAny
v5 ~AgdaAny
v6 T_ReflClosure_30
v7
  = (AgdaAny -> AgdaAny) -> AgdaAny -> T_ReflClosure_30 -> AgdaAny
du_drop'45'refl_62 AgdaAny -> AgdaAny
v4 AgdaAny
v5 T_ReflClosure_30
v7
du_drop'45'refl_62 ::
  (AgdaAny -> AgdaAny) -> AgdaAny -> T_ReflClosure_30 -> AgdaAny
du_drop'45'refl_62 :: (AgdaAny -> AgdaAny) -> AgdaAny -> T_ReflClosure_30 -> AgdaAny
du_drop'45'refl_62 AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_ReflClosure_30
v2
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v2 of
      T_ReflClosure_30
C_refl_36 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
      C_'91'_'93'_44 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
      T_ReflClosure_30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.reflexive
d_reflexive_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_ReflClosure_30
d_reflexive_72 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_ReflClosure_30
d_reflexive_72 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~T__'8801'__12
v6 = T_ReflClosure_30
du_reflexive_72
du_reflexive_72 :: T_ReflClosure_30
du_reflexive_72 :: T_ReflClosure_30
du_reflexive_72 = T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
C_refl_36
-- Relation.Binary.Construct.Closure.Reflexive.[]-injective
d_'91''93''45'injective_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91''93''45'injective_84 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91''93''45'injective_84 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Refl
d_Refl_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_Refl_96 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
d_Refl_96 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> ()
forall a. a
erased