Documentation

d_Error_2 ∷ () Source #

data T_Error_2 Source #

d_tagToRelation_12 ∷ T_CertifiedOptTag_12 → T__'8866'_14 → T__'8866'_14 → () Source #

d_RelationOf_14 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → T__'8866'_14 → T__'8866'_14 → () Source #

d_hasRelation_18 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → Bool Source #

d_certifyPass_26 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → T_Hints_92 T__'8866'_14 → T__'8866'_14 → T__'8866'_14 → T_CertResult_12 Source #

d_Certificate_34 ∷ T_NonEmptySep_104 (T__'215'__436 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) (T_Hints_92 T__'8866'_14)) T__'8866'_14 → () Source #

d_certify_46 ∷ T_NonEmptySep_104 (T__'215'__436 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) (T_Hints_92 T__'8866'_14)) T__'8866'_14 → T_Either_6 T_Error_2 AgdaAny Source #

d_cert_96 ∷ T_NonEmptySep_104 (T__'215'__436 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) (T_Hints_92 T__'8866'_14)) T__'8866'_14 → T_Either_6 T_Error_2 AgdaAny → AgdaAny → AgdaAny Source #

du_cert_96 ∷ T_Either_6 T_Error_2 AgdaAny → AgdaAny → AgdaAny Source #

d_checkScope_100 ∷ T_Untyped_210 → Maybe T__'8866'_14 Source #

d_checkScope'738'_102 ∷ T_InlineHints'8314'_82 T_Untyped_210 → Maybe (T_InlineHints'8314'_82 T__'8866'_14) Source #

d_checkScope'688'_116 ∷ T_Hints_92 T_Untyped_210 → Maybe (T_Hints_92 T__'8866'_14) Source #

d_checkScope'7511'_122 ∷ T_NonEmptySep_104 (T__'215'__436 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) (T_Hints_92 T_Untyped_210)) T_Untyped_210 → Maybe (T_NonEmptySep_104 (T__'215'__436 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) (T_Hints_92 T__'8866'_14)) T__'8866'_14) Source #