| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.Certificate
Documentation
d_CertResult_12 :: p -> p -> () #
data T_CertResult_12 #
d_ProofOrCE_38 :: p -> p -> () #
data T_ProofOrCE_38 #
Constructors
| C_proof_44 AgdaAny | |
| C_ce_52 T_SimplifierTag_4 AgdaAny AgdaAny |
d_Proof'63'_58 :: p -> p -> () #
data T_Proof'63'_58 #
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 #
du__'62''62''61'__80 :: T_Proof'63'_58 -> (AgdaAny -> T_Proof'63'_58) -> T_Proof'63'_58 #
d_DecidableCE_100 :: () -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> () #
d_Checkable_118 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> () #
d_Certifiable_134 :: () -> (AgdaAny -> AgdaAny -> ()) -> () #
d_checker_148 :: () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Proof'63'_58) -> AgdaAny -> AgdaAny -> T_CertResult_12 #
du_checker_148 :: (AgdaAny -> AgdaAny -> T_Proof'63'_58) -> AgdaAny -> AgdaAny -> T_CertResult_12 #
d_decider_184 :: () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny -> T_CertResult_12 #
du_decider_184 :: (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> AgdaAny -> AgdaAny -> T_CertResult_12 #
d_decToPCE_226 :: () -> () -> T_SimplifierTag_4 -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 #
du_decToPCE_226 :: T_SimplifierTag_4 -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 #
d_pceToDec_240 :: () -> T_ProofOrCE_38 -> T_Dec_20 #
d_matchOrCE_254 :: () -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_SimplifierTag_4 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 #
du_matchOrCE_254 :: T_SimplifierTag_4 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_ProofOrCE_38 #
d_pcePointwise_296 :: () -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_SimplifierTag_4 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38 #
du_pcePointwise_296 :: T_SimplifierTag_4 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_38) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_38 #