{-# 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.VerifiedCompilation.Purity 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.Bool
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped

-- VerifiedCompilation.Purity.UPure
d_UPure_6 :: p -> p -> ()
d_UPure_6 p
a0 p
a1 = ()
data T_UPure_6 = C_FIXME_12
-- VerifiedCompilation.Purity.isUPure?
d_isUPure'63'_18 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isUPure'63'_18 :: T__'8866'_14 -> T_Dec_20
d_isUPure'63'_18 ~T__'8866'_14
v0 = T_Dec_20
du_isUPure'63'_18
du_isUPure'63'_18 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isUPure'63'_18 :: T_Dec_20
du_isUPure'63'_18
  = (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
      (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
      ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
         Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
         (T_UPure_6 -> Any
forall a b. a -> b
coe T_UPure_6
C_FIXME_12))