{-# 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.Tree.AVL.Value 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles

-- Data.Tree.AVL.Value.Value
d_Value_38 :: p -> p -> p -> p -> ()
d_Value_38 p
a0 p
a1 p
a2 p
a3 = ()
newtype T_Value_38
  = C_MkValue_50 (AgdaAny ->
                  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Data.Tree.AVL.Value.Value.family
d_family_46 :: T_Value_38 -> AgdaAny -> ()
d_family_46 :: T_Value_38 -> AgdaAny -> ()
d_family_46 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL.Value.Value.respects
d_respects_48 ::
  T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_48 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_48 T_Value_38
v0
  = case T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
v0 of
      C_MkValue_50 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_Value_38
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.K&_
d_K'38'__56 :: p -> p -> p -> p -> p -> ()
d_K'38'__56 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_K'38'__56 = C__'44'__70 AgdaAny AgdaAny
-- Data.Tree.AVL.Value.K&_.key
d_key_66 :: T_K'38'__56 -> AgdaAny
d_key_66 :: T_K'38'__56 -> AgdaAny
d_key_66 T_K'38'__56
v0
  = case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v0 of
      C__'44'__70 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.K&_.value
d_value_68 :: T_K'38'__56 -> AgdaAny
d_value_68 :: T_K'38'__56 -> AgdaAny
d_value_68 T_K'38'__56
v0
  = case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v0 of
      C__'44'__70 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value._.toPair
d_toPair_80 ::
  T_K'38'__56 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_80 :: T_K'38'__56 -> T_Σ_14
d_toPair_80 T_K'38'__56
v0
  = case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v0 of
      C__'44'__70 AgdaAny
v1 AgdaAny
v2
        -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      T_K'38'__56
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value._.fromPair
d_fromPair_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Value_38 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_K'38'__56
d_fromPair_86 :: ()
-> () -> T_Setoid_44 -> () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
d_fromPair_86 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~T_Value_38
v4 T_Σ_14
v5 = T_Σ_14 -> T_K'38'__56
du_fromPair_86 T_Σ_14
v5
du_fromPair_86 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_K'38'__56
du_fromPair_86 :: T_Σ_14 -> T_K'38'__56
du_fromPair_86 T_Σ_14
v0
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v1 AgdaAny
v2
        -> (AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> T_K'38'__56
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_K'38'__56
C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      T_Σ_14
_ -> T_K'38'__56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.const
d_const_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Value_38
d_const_94 :: () -> () -> T_Setoid_44 -> () -> () -> T_Value_38
d_const_94 ~()
v0 ~()
v1 ~T_Setoid_44
v2 ~()
v3 ~()
v4 = T_Value_38
du_const_94
du_const_94 :: T_Value_38
du_const_94 :: T_Value_38
du_const_94
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Value_38)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_38
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_38
C_MkValue_50 (\ AgdaAny
v0 AgdaAny
v1 -> let v2 :: p -> p
v2 = \ p
v2 -> p
v2 in (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny -> AgdaAny
forall {p}. p -> p
v2))