| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.Certificate
Documentation
d_CertResult_12 ∷ p → p → () Source #
data T_CertResult_12 Source #
d_ProofOrCE_38 ∷ p → p → () Source #
data T_ProofOrCE_38 Source #
d_isProof'63'_56 ∷ T_Level_18 → () → T_ProofOrCE_38 → Bool Source #
d_isCE'63'_60 ∷ T_Level_18 → () → T_ProofOrCE_38 → Bool Source #
d_Proof'63'_66 ∷ p → p → () Source #
data T_Proof'63'_66 Source #
d__'62''62''61'__88 ∷ T_Level_18 → T_Level_18 → () → () → T_Proof'63'_66 → (AgdaAny → T_Proof'63'_66) → T_Proof'63'_66 Source #
d_DecidableCE_108 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Checkable_126 ∷ () → () → (AgdaAny → AgdaAny → ()) → () Source #
d_Certifiable_142 ∷ () → (AgdaAny → AgdaAny → ()) → () Source #
d_checker_156 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Proof'63'_66) → AgdaAny → AgdaAny → T_CertResult_12 Source #
du_checker_156 ∷ (AgdaAny → AgdaAny → T_Proof'63'_66) → AgdaAny → AgdaAny → T_CertResult_12 Source #
d_decider_192 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_ProofOrCE_38) → AgdaAny → AgdaAny → T_CertResult_12 Source #
du_decider_192 ∷ (AgdaAny → AgdaAny → T_ProofOrCE_38) → AgdaAny → AgdaAny → T_CertResult_12 Source #
d_decToPCE_234 ∷ () → () → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
du_decToPCE_234 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
d_pceToDec_248 ∷ () → T_ProofOrCE_38 → T_Dec_20 Source #
d_matchOrCE_262 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
du_matchOrCE_262 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
d_pcePointwise_304 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (AgdaAny → AgdaAny → T_ProofOrCE_38) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_38 Source #