Documentation

d_Transformation_2 ∷ p → p → p → p → p → () Source #

data T_Transformation_2 Source #

d_Trace_68 ∷ p → p → p → () Source #

data T_Trace_68 Source #

d_isTransformation'63'_96 ∷ () → T_DecEq_6 → T_SimplifierTag_4 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

du_isTransformation'63'_96 ∷ T_DecEq_6 → T_SimplifierTag_4 → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_26 Source #

d_isTrace'63'_300 ∷ () → T_DecEq_6 → T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 T__'8866'_14 T__'8866'_14)) → T_ProofOrCE_26 Source #

du_isTrace'63'_300 ∷ T_DecEq_6 → T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 T__'8866'_14 T__'8866'_14)) → T_ProofOrCE_26 Source #

type T_FileHandle_396 = Handle Source #

d_FileHandle_396 ∷ a Source #

d_writeFile_398 ∷ T_String_6 → T_String_6 → T_IO_8 () T_'8868'_6 Source #

d_stderr_400 ∷ T_FileHandle_396 Source #

d_hPutStrLn_402 ∷ T_FileHandle_396 → T_String_6 → T_IO_8 () T_'8868'_6 Source #

d_putStrLn_404 ∷ T_String_6 → T_IO_8 () T_'8868'_6 Source #

d_buildPairs_408 ∷ () → T_List_384 T__'8866'_14 → T_List_384 (T__'215'__366 T__'8866'_14 T__'8866'_14) Source #

du_buildPairs_408 ∷ T_List_384 T__'8866'_14 → T_List_384 (T__'215'__366 T__'8866'_14 T__'8866'_14) Source #

d_traverseEitherList_424 ∷ () → () → () → (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 AgdaAny AgdaAny)) → T_Either_6 AgdaAny (T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 AgdaAny AgdaAny))) Source #

du_traverseEitherList_424 ∷ (AgdaAny → T_Either_6 AgdaAny AgdaAny) → T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 AgdaAny AgdaAny)) → T_Either_6 AgdaAny (T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 AgdaAny AgdaAny))) Source #

d_Cert_532 ∷ () Source #

data T_Cert_532 Source #

d_runCertifier_542 ∷ T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 T_Untyped_146 T_Untyped_146)) → Maybe T_Cert_532 Source #

d_getCE_564 ∷ () → () → Maybe T_Cert_532 → Maybe T_Σ_14 Source #

du_getCE_564 ∷ Maybe T_Cert_532 → Maybe T_Σ_14 Source #

d_passed'63'_576 ∷ Maybe T_Cert_532 → Bool Source #

runCertifierMain ∷ T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 T_Untyped_146 T_Untyped_146)) → T_Maybe_10 () Bool Source #

d_runCertifierMain_578 ∷ T_List_384 (T__'215'__366 T_SimplifierTag_4 (T__'215'__366 T_Untyped_146 T_Untyped_146)) → Maybe Bool Source #