{-# 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_40 :: p -> p -> p -> p -> ()
d_Value_40 p
a0 p
a1 p
a2 p
a3 = ()
newtype T_Value_40
  = C_MkValue_52 (AgdaAny ->
                  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Data.Tree.AVL.Value.Value.family
d_family_48 :: T_Value_40 -> AgdaAny -> ()
d_family_48 :: T_Value_40 -> AgdaAny -> ()
d_family_48 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL.Value.Value.respects
d_respects_50 ::
  T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_50 :: T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_50 T_Value_40
v0
  = case T_Value_40 -> T_Value_40
forall a b. a -> b
coe T_Value_40
v0 of
      C_MkValue_52 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_40
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.K&_
d_K'38'__58 :: p -> p -> p -> p -> p -> ()
d_K'38'__58 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_K'38'__58 = C__'44'__72 AgdaAny AgdaAny
-- Data.Tree.AVL.Value.K&_.key
d_key_68 :: T_K'38'__58 -> AgdaAny
d_key_68 :: T_K'38'__58 -> AgdaAny
d_key_68 T_K'38'__58
v0
  = case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v0 of
      C__'44'__72 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_K'38'__58
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.K&_.value
d_value_70 :: T_K'38'__58 -> AgdaAny
d_value_70 :: T_K'38'__58 -> AgdaAny
d_value_70 T_K'38'__58
v0
  = case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v0 of
      C__'44'__72 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_K'38'__58
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value._.toPair
d_toPair_82 ::
  T_K'38'__58 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_82 :: T_K'38'__58 -> T_Σ_14
d_toPair_82 T_K'38'__58
v0
  = case T_K'38'__58 -> T_K'38'__58
forall a b. a -> b
coe T_K'38'__58
v0 of
      C__'44'__72 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'__58
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value._.fromPair
d_fromPair_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  T_Value_40 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_K'38'__58
d_fromPair_88 :: ()
-> () -> T_Setoid_46 -> () -> T_Value_40 -> T_Σ_14 -> T_K'38'__58
d_fromPair_88 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~T_Value_40
v4 T_Σ_14
v5 = T_Σ_14 -> T_K'38'__58
du_fromPair_88 T_Σ_14
v5
du_fromPair_88 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_K'38'__58
du_fromPair_88 :: T_Σ_14 -> T_K'38'__58
du_fromPair_88 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'__58)
-> AgdaAny -> AgdaAny -> T_K'38'__58
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_K'38'__58
C__'44'__72 (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'__58
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Value.const
d_const_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Value_40
d_const_96 :: () -> () -> T_Setoid_46 -> () -> () -> T_Value_40
d_const_96 ~()
v0 ~()
v1 ~T_Setoid_46
v2 ~()
v3 ~()
v4 = T_Value_40
du_const_96
du_const_96 :: T_Value_40
du_const_96 :: T_Value_40
du_const_96
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Value_40)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_40
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_40
C_MkValue_52 (\ 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))