{-# 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.Certificate 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.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.VerifiedCompilation.Trace

-- VerifiedCompilation.Certificate.CertResult
d_CertResult_12 :: p -> p -> ()
d_CertResult_12 p
a0 p
a1 = ()
data T_CertResult_12
  = C_proof_18 AgdaAny |
    C_ce_26 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
            AgdaAny AgdaAny |
    C_abort_32 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.ProofOrCE
d_ProofOrCE_38 :: p -> p -> ()
d_ProofOrCE_38 p
a0 p
a1 = ()
data T_ProofOrCE_38
  = C_proof_44 AgdaAny |
    C_ce_52 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
            AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.isProof?
d_isProof'63'_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_ProofOrCE_38 -> Bool
d_isProof'63'_56 :: () -> () -> T_ProofOrCE_38 -> Bool
d_isProof'63'_56 ~()
v0 ~()
v1 T_ProofOrCE_38
v2 = T_ProofOrCE_38 -> Bool
du_isProof'63'_56 T_ProofOrCE_38
v2
du_isProof'63'_56 :: T_ProofOrCE_38 -> Bool
du_isProof'63'_56 :: T_ProofOrCE_38 -> Bool
du_isProof'63'_56 T_ProofOrCE_38
v0
  = case T_ProofOrCE_38 -> T_ProofOrCE_38
forall a b. a -> b
coe T_ProofOrCE_38
v0 of
      C_proof_44 AgdaAny
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      C_ce_52 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      T_ProofOrCE_38
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.isCE?
d_isCE'63'_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_ProofOrCE_38 -> Bool
d_isCE'63'_60 :: () -> () -> T_ProofOrCE_38 -> Bool
d_isCE'63'_60 ~()
v0 ~()
v1 T_ProofOrCE_38
v2 = T_ProofOrCE_38 -> Bool
du_isCE'63'_60 T_ProofOrCE_38
v2
du_isCE'63'_60 :: T_ProofOrCE_38 -> Bool
du_isCE'63'_60 :: T_ProofOrCE_38 -> Bool
du_isCE'63'_60 T_ProofOrCE_38
v0
  = (Bool -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
      Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
      ((T_ProofOrCE_38 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ProofOrCE_38 -> Bool
du_isProof'63'_56 (T_ProofOrCE_38 -> AgdaAny
forall a b. a -> b
coe T_ProofOrCE_38
v0))
-- VerifiedCompilation.Certificate.Proof?
d_Proof'63'_66 :: p -> p -> ()
d_Proof'63'_66 p
a0 p
a1 = ()
data T_Proof'63'_66
  = C_proof_72 AgdaAny |
    C_abort_78 MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate._>>=_
d__'62''62''61'__88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
d__'62''62''61'__88 :: ()
-> ()
-> ()
-> ()
-> T_Proof'63'_66
-> (AgdaAny -> T_Proof'63'_66)
-> T_Proof'63'_66
d__'62''62''61'__88 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Proof'63'_66
v4 AgdaAny -> T_Proof'63'_66
v5
  = T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
du__'62''62''61'__88 T_Proof'63'_66
v4 AgdaAny -> T_Proof'63'_66
v5
du__'62''62''61'__88 ::
  T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
du__'62''62''61'__88 :: T_Proof'63'_66 -> (AgdaAny -> T_Proof'63'_66) -> T_Proof'63'_66
du__'62''62''61'__88 T_Proof'63'_66
v0 AgdaAny -> T_Proof'63'_66
v1
  = case T_Proof'63'_66 -> T_Proof'63'_66
forall a b. a -> b
coe T_Proof'63'_66
v0 of
      C_proof_72 AgdaAny
v2 -> (AgdaAny -> T_Proof'63'_66) -> AgdaAny -> T_Proof'63'_66
forall a b. a -> b
coe AgdaAny -> T_Proof'63'_66
v1 AgdaAny
v2
      C_abort_78 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_66)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_66
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_Proof'63'_66
C_abort_78 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6
      T_Proof'63'_66
_ -> T_Proof'63'_66
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.DecidableCE
d_DecidableCE_108 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_108 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_108 = () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Checkable
d_Checkable_126 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_126 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_126 = () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Certifiable
d_Certifiable_142 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_142 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_142 = () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.checker
d_checker_156 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_Proof'63'_66) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_checker_156 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Proof'63'_66)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_checker_156 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_Proof'63'_66
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Proof'63'_66)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_156 AgdaAny -> AgdaAny -> T_Proof'63'_66
v2 AgdaAny
v3 AgdaAny
v4
du_checker_156 ::
  (AgdaAny -> AgdaAny -> T_Proof'63'_66) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_156 :: (AgdaAny -> AgdaAny -> T_Proof'63'_66)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_156 AgdaAny -> AgdaAny -> T_Proof'63'_66
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Proof'63'_66)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Proof'63'_66
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_Proof'63'_66
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_72 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_abort_78 T_SimplifierTag_4
v6 AgdaAny
v7 AgdaAny
v8 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12
C_abort_32 T_SimplifierTag_4
v6 AgdaAny
v7 AgdaAny
v8
         T_Proof'63'_66
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decider
d_decider_192 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_decider_192 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_decider_192 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_192 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v2 AgdaAny
v3 AgdaAny
v4
du_decider_192 ::
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_192 :: (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_192 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_44 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_ce_52 T_SimplifierTag_4
v7 AgdaAny
v8 AgdaAny
v9 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_CertResult_12
C_ce_26 T_SimplifierTag_4
v7 AgdaAny
v8 AgdaAny
v9
         T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_234 ::
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_decToPCE_234 :: ()
-> ()
-> T_SimplifierTag_4
-> T_Dec_20
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
d_decToPCE_234 ~()
v0 ~()
v1 T_SimplifierTag_4
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5 = T_SimplifierTag_4
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_234 T_SimplifierTag_4
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5
du_decToPCE_234 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_234 :: T_SimplifierTag_4
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_decToPCE_234 T_SimplifierTag_4
v0 T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v6
                      -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_38
C_proof_44 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                    T_Reflects_16
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5) ((T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 AgdaAny
v2 AgdaAny
v3)
      T_Dec_20
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_248 ::
  () ->
  T_ProofOrCE_38 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_248 :: () -> T_ProofOrCE_38 -> T_Dec_20
d_pceToDec_248 ~()
v0 T_ProofOrCE_38
v1 = T_ProofOrCE_38 -> T_Dec_20
du_pceToDec_248 T_ProofOrCE_38
v1
du_pceToDec_248 ::
  T_ProofOrCE_38 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_248 :: T_ProofOrCE_38 -> T_Dec_20
du_pceToDec_248 T_ProofOrCE_38
v0
  = case T_ProofOrCE_38 -> T_ProofOrCE_38
forall a b. a -> b
coe T_ProofOrCE_38
v0 of
      C_proof_44 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      C_ce_52 T_SimplifierTag_4
v4 AgdaAny
v5 AgdaAny
v6
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
      T_ProofOrCE_38
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_262 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
d_matchOrCE_262 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
d_matchOrCE_262 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
  = T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
du_matchOrCE_262 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_matchOrCE_262 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_38
du_matchOrCE_262 :: T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_38
du_matchOrCE_262 T_SimplifierTag_4
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 in
    AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
      (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v4 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v7
                         -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_38
C_proof_44 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
                       T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6) ((T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 AgdaAny
v2 AgdaAny
v3)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_304 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
d_pcePointwise_304 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
d_pcePointwise_304 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v5 [AgdaAny]
v6 [AgdaAny]
v7
  = T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_304 T_SimplifierTag_4
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_pcePointwise_304 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_38) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
du_pcePointwise_304 :: T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_304 T_SimplifierTag_4
v0 AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
                    AgdaAny -> T_ProofOrCE_38
C_proof_44
                    (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
                       T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
             (:) AgdaAny
v4 [AgdaAny]
v5 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 [AgdaAny]
v2 [AgdaAny]
v5
             [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             [] -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v0 [AgdaAny]
v5 [AgdaAny]
v3
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe
                    (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v8 of
                       C_proof_44 AgdaAny
v9
                         -> let v10 :: AgdaAny
v10
                                  = (T_SimplifierTag_4
 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_ProofOrCE_38)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_38
du_pcePointwise_304 (T_SimplifierTag_4 -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4
v0) ((AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_38
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_ProofOrCE_38
forall a b. a -> b
coe AgdaAny
v10 of
                                 C_proof_44 AgdaAny
v11
                                   -> (AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_ProofOrCE_38
C_proof_44
                                        ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                           AgdaAny
v9 AgdaAny
v11)
                                 C_ce_52 T_SimplifierTag_4
v14 AgdaAny
v15 AgdaAny
v16 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v14 AgdaAny
v15 AgdaAny
v16
                                 T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       C_ce_52 T_SimplifierTag_4
v12 AgdaAny
v13 AgdaAny
v14 -> (T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38)
-> T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_SimplifierTag_4 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38
C_ce_52 T_SimplifierTag_4
v12 AgdaAny
v13 AgdaAny
v14
                       T_ProofOrCE_38
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_ProofOrCE_38
forall a. a
MAlonzo.RTE.mazUnreachableError