| 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 #
Constructors
| C_proof_44 AgdaAny | |
| C_ce_52 T_SimplifierTag_4 AgdaAny AgdaAny |
d_Proof'63'_58 ∷ p → p → () Source #
data T_Proof'63'_58 Source #
Constructors
| C_proof_64 AgdaAny | |
| C_abort_70 T_SimplifierTag_4 AgdaAny AgdaAny |
d__'62''62''61'__80 ∷ T_Level_18 → T_Level_18 → () → () → T_Proof'63'_58 → (AgdaAny → T_Proof'63'_58) → T_Proof'63'_58 Source #
d_DecidableCE_100 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Checkable_118 ∷ () → () → (AgdaAny → AgdaAny → ()) → () Source #
d_Certifiable_134 ∷ () → (AgdaAny → AgdaAny → ()) → () Source #
d_checker_148 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Proof'63'_58) → AgdaAny → AgdaAny → T_CertResult_12 Source #
du_checker_148 ∷ (AgdaAny → AgdaAny → T_Proof'63'_58) → AgdaAny → AgdaAny → T_CertResult_12 Source #
d_decider_184 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_ProofOrCE_38) → AgdaAny → AgdaAny → T_CertResult_12 Source #
du_decider_184 ∷ (AgdaAny → AgdaAny → T_ProofOrCE_38) → AgdaAny → AgdaAny → T_CertResult_12 Source #
d_decToPCE_226 ∷ () → () → T_SimplifierTag_4 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
d_pceToDec_240 ∷ () → T_ProofOrCE_38 → T_Dec_20 Source #
d_matchOrCE_254 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
du_matchOrCE_254 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_38 Source #
d_pcePointwise_296 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_38) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_38 Source #
du_pcePointwise_296 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_38) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_38 Source #