{-# 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.NotImplemented 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.Untyped
import qualified MAlonzo.Code.VerifiedCompilation.Certificate

-- VerifiedCompilation.NotImplemented.Policy
d_Policy_4 :: ()
d_Policy_4 = ()
data T_Policy_4 = C_accept_6 | C_reject_8
-- VerifiedCompilation.NotImplemented.NotImplemented
d_NotImplemented_12 :: p -> p -> p -> p -> ()
d_NotImplemented_12 p
a0 p
a1 p
a2 p
a3 = ()
data T_NotImplemented_12 = C_notImplemented_20
-- VerifiedCompilation.NotImplemented.certNotImplemented
d_certNotImplemented_22 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_CertResult_12
d_certNotImplemented_22 :: T__'8866'_14 -> T__'8866'_14 -> T_CertResult_12
d_certNotImplemented_22 ~T__'8866'_14
v0 ~T__'8866'_14
v1 = T_CertResult_12
du_certNotImplemented_22
du_certNotImplemented_22 ::
  MAlonzo.Code.VerifiedCompilation.Certificate.T_CertResult_12
du_certNotImplemented_22 :: T_CertResult_12
du_certNotImplemented_22
  = (Any -> T_CertResult_12) -> Any -> T_CertResult_12
forall a b. a -> b
coe
      Any -> T_CertResult_12
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_18
      (T_NotImplemented_12 -> Any
forall a b. a -> b
coe T_NotImplemented_12
C_notImplemented_20)