| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation
Documentation
d_Transformation_2 ∷ p → p → p → p → () Source #
data T_Transformation_2 Source #
d_Trace_60 ∷ p → p → () Source #
data T_Trace_60 Source #
Constructors
| C_empty_64 | |
| C_cons_78 T_Transformation_2 T_Trace_60 |
d_isTransformation'63'_90 ∷ Integer → T_SimplifierTag_4 → T_Hints_46 → T__'8866'_14 → T__'8866'_14 → T_CertResult_60 Source #
d_isTrace'63'_362 ∷ Integer → T_List_414 (T__'215'__396 T_SimplifierTag_4 (T__'215'__396 T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14))) → T_CertResult_60 Source #
type T_FileHandle_506 = Handle Source #
d_FileHandle_506 ∷ a Source #
d_writeFile_508 ∷ T_String_6 → T_String_6 → T_IO_8 () T_'8868'_6 Source #
d_putStrLn_514 ∷ T_String_6 → T_IO_8 () T_'8868'_6 Source #
d_buildPairs_518 ∷ Integer → T_List_414 T__'8866'_14 → T_List_414 (T__'215'__396 T__'8866'_14 T__'8866'_14) Source #
du_buildPairs_518 ∷ T_List_414 T__'8866'_14 → T_List_414 (T__'215'__396 T__'8866'_14 T__'8866'_14) Source #
d_traverseEitherList_534 ∷ () → () → () → (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_List_414 (T__'215'__396 T_SimplifierTag_4 (T__'215'__396 T_Hints_46 (T__'215'__396 AgdaAny AgdaAny))) → T_Either_6 AgdaAny (T_List_414 (T__'215'__396 T_SimplifierTag_4 (T__'215'__396 T_Hints_46 (T__'215'__396 AgdaAny AgdaAny)))) Source #
du_traverseEitherList_534 ∷ (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_List_414 (T__'215'__396 T_SimplifierTag_4 (T__'215'__396 T_Hints_46 (T__'215'__396 AgdaAny AgdaAny))) → T_Either_6 AgdaAny (T_List_414 (T__'215'__396 T_SimplifierTag_4 (T__'215'__396 T_Hints_46 (T__'215'__396 AgdaAny AgdaAny)))) Source #
d_Cert_656 ∷ () Source #
data T_Cert_656 Source #
d_getCE_672 ∷ () → () → Maybe T_Cert_656 → Maybe T_Σ_14 Source #