{-# 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.Height 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.Data.Fin.Base

-- Data.Tree.AVL.Height.ℕ₂
d_ℕ'8322'_8 :: ()
d_ℕ'8322'_8 :: ()
d_ℕ'8322'_8 = ()
forall a. a
erased
-- Data.Tree.AVL.Height._⊕_
d__'8853'__16 ::
  MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> Integer -> Integer
d__'8853'__16 :: T_Fin_6 -> Integer -> Integer
d__'8853'__16 T_Fin_6
v0 Integer
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
      T_Fin_6
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Height.pred[_⊕_]
d_pred'91'_'8853'_'93'_22 ::
  MAlonzo.Code.Data.Fin.Base.T_Fin_6 -> Integer -> Integer
d_pred'91'_'8853'_'93'_22 :: T_Fin_6 -> Integer -> Integer
d_pred'91'_'8853'_'93'_22 T_Fin_6
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe ((T_Fin_6 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Integer -> Integer
d__'8853'__16 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
-- Data.Tree.AVL.Height._∼_⊔_
d__'8764'_'8852'__30 :: p -> p -> p -> ()
d__'8764'_'8852'__30 p
a0 p
a1 p
a2 = ()
data T__'8764'_'8852'__30
  = C_'8764''43'_34 | C_'8764'0_38 | C_'8764''45'_42
-- Data.Tree.AVL.Height.max∼
d_max'8764'_50 ::
  Integer ->
  Integer -> Integer -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
d_max'8764'_50 :: Integer
-> Integer
-> Integer
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
d_max'8764'_50 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8764'_'8852'__30
v3 = T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_max'8764'_50 T__'8764'_'8852'__30
v3
du_max'8764'_50 :: T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_max'8764'_50 :: T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_max'8764'_50 T__'8764'_'8852'__30
v0
  = case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v0 of
      T__'8764'_'8852'__30
C_'8764''43'_34 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764''45'_42
      T__'8764'_'8852'__30
C_'8764'0_38 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764'0_38
      T__'8764'_'8852'__30
C_'8764''45'_42 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764'0_38
      T__'8764'_'8852'__30
_ -> T__'8764'_'8852'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Height.∼max
d_'8764'max_58 ::
  Integer ->
  Integer -> Integer -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
d_'8764'max_58 :: Integer
-> Integer
-> Integer
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
d_'8764'max_58 ~Integer
v0 ~Integer
v1 ~Integer
v2 T__'8764'_'8852'__30
v3 = T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_'8764'max_58 T__'8764'_'8852'__30
v3
du_'8764'max_58 :: T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_'8764'max_58 :: T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
du_'8764'max_58 T__'8764'_'8852'__30
v0
  = case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v0 of
      T__'8764'_'8852'__30
C_'8764''43'_34 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764'0_38
      T__'8764'_'8852'__30
C_'8764'0_38 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764'0_38
      T__'8764'_'8852'__30
C_'8764''45'_42 -> T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
C_'8764''43'_34
      T__'8764'_'8852'__30
_ -> T__'8764'_'8852'__30
forall a. a
MAlonzo.RTE.mazUnreachableError