| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.Certificate
Documentation
d_SimplifierTag_4 ∷ () Source #
type T_SimplifierTag_4 = SimplifierStage Source #
pattern C_floatDelayT_6 ∷ SimplifierStage Source #
pattern C_forceDelayT_8 ∷ SimplifierStage Source #
pattern C_forceCaseDelayT_10 ∷ SimplifierStage Source #
pattern C_caseOfCaseT_12 ∷ SimplifierStage Source #
pattern C_caseReduceT_14 ∷ SimplifierStage Source #
pattern C_inlineT_16 ∷ SimplifierStage Source #
pattern C_cseT_18 ∷ SimplifierStage Source #
d_CertResult_28 ∷ p → p → () Source #
data T_CertResult_28 Source #
d_ProofOrCE_54 ∷ p → p → () Source #
data T_ProofOrCE_54 Source #
Constructors
| C_proof_60 AgdaAny | |
| C_ce_68 T_SimplifierTag_4 AgdaAny AgdaAny |
d_Proof'63'_74 ∷ p → p → () Source #
data T_Proof'63'_74 Source #
Constructors
| C_proof_80 AgdaAny | |
| C_abort_86 T_SimplifierTag_4 AgdaAny AgdaAny |
d_decToPCE_96 ∷ () → () → T_SimplifierTag_4 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_54 Source #
d_pceToDec_110 ∷ () → T_ProofOrCE_54 → T_Dec_20 Source #
d_MatchOrCE_124 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_matchOrCE_144 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_54 Source #
du_matchOrCE_144 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_54 Source #
d_pcePointwise_186 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_54) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_54 Source #
du_pcePointwise_186 ∷ T_SimplifierTag_4 → (AgdaAny → AgdaAny → T_ProofOrCE_54) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_54 Source #