{-# 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.Level 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.Primitive

-- Level.Lift
d_Lift_8 :: p -> p -> p -> ()
d_Lift_8 p
a0 p
a1 p
a2 = ()
newtype T_Lift_8 = C_lift_20 AgdaAny
-- Level.Lift.lower
d_lower_18 :: T_Lift_8 -> AgdaAny
d_lower_18 :: T_Lift_8 -> AgdaAny
d_lower_18 T_Lift_8
v0
  = case T_Lift_8 -> T_Lift_8
forall a b. a -> b
coe T_Lift_8
v0 of
      C_lift_20 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Lift_8
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Level.0ℓ
d_0ℓ_22 :: MAlonzo.Code.Agda.Primitive.T_Level_18
d_0ℓ_22 :: ()
d_0ℓ_22 = () -> ()
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Primitive.d_lzero_20
-- Level.levelOfType
d_levelOfType_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_levelOfType_26 :: () -> () -> ()
d_levelOfType_26 ()
v0 ~()
v1 = () -> ()
du_levelOfType_26 ()
v0
du_levelOfType_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18
du_levelOfType_26 :: () -> ()
du_levelOfType_26 ()
v0 = () -> ()
forall a b. a -> b
coe ()
v0
-- Level.levelOfTerm
d_levelOfTerm_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_levelOfTerm_34 :: () -> () -> AgdaAny -> ()
d_levelOfTerm_34 ()
v0 ~()
v1 ~AgdaAny
v2 = () -> ()
du_levelOfTerm_34 ()
v0
du_levelOfTerm_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18
du_levelOfTerm_34 :: () -> ()
du_levelOfTerm_34 ()
v0 = () -> ()
forall a b. a -> b
coe ()
v0