Documentation

d_CertResult_12 ∷ p → p → () Source #

data T_CertResult_12 Source #

d_is'45'proof_36 ∷ T_Level_18 → () → T_CertResult_12 → Bool Source #

du_is'45'proof_36 ∷ T_CertResult_12 → Bool Source #

d_to'45'witness'45'T_42 ∷ T_Level_18 → () → T_CertResult_12 → AgdaAny → AgdaAny Source #

du_to'45'witness'45'T_42 ∷ T_CertResult_12 → AgdaAny Source #

d_ProofOrCE_50 ∷ p → p → () Source #

data T_ProofOrCE_50 Source #

d_isProof'63'_68 ∷ T_Level_18 → () → T_ProofOrCE_50 → Bool Source #

du_isProof'63'_68 ∷ T_ProofOrCE_50 → Bool Source #

d_isCE'63'_72 ∷ T_Level_18 → () → T_ProofOrCE_50 → Bool Source #

du_isCE'63'_72 ∷ T_ProofOrCE_50 → Bool Source #

d_Proof'63'_78 ∷ p → p → () Source #

data T_Proof'63'_78 Source #

d__'62''62''61'__100 ∷ T_Level_18 → T_Level_18 → () → () → T_Proof'63'_78 → (AgdaAny → T_Proof'63'_78) → T_Proof'63'_78 Source #

du__'62''62''61'__100 ∷ T_Proof'63'_78 → (AgdaAny → T_Proof'63'_78) → T_Proof'63'_78 Source #

d_DecidableCE_120 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_Checkable_138 ∷ () → () → (AgdaAny → AgdaAny → ()) → () Source #

d_Certifiable_154 ∷ () → (AgdaAny → AgdaAny → ()) → () Source #

d_checker_168 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Proof'63'_78) → AgdaAny → AgdaAny → T_CertResult_12 Source #

du_checker_168 ∷ (AgdaAny → AgdaAny → T_Proof'63'_78) → AgdaAny → AgdaAny → T_CertResult_12 Source #

d_decider_204 ∷ () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_ProofOrCE_50) → AgdaAny → AgdaAny → T_CertResult_12 Source #

du_decider_204 ∷ (AgdaAny → AgdaAny → T_ProofOrCE_50) → AgdaAny → AgdaAny → T_CertResult_12 Source #

d_decToPCE_246 ∷ () → () → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_50 Source #

du_decToPCE_246 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → T_Dec_20 → AgdaAny → AgdaAny → T_ProofOrCE_50 Source #

d_pceToDec_260 ∷ () → T_ProofOrCE_50 → T_Dec_20 Source #

du_pceToDec_260 ∷ T_ProofOrCE_50 → T_Dec_20 Source #

d_matchOrCE_274 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_50 Source #

du_matchOrCE_274 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_ProofOrCE_50 Source #

d_pcePointwise_316 ∷ () → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → (AgdaAny → AgdaAny → T_ProofOrCE_50) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_50 Source #

du_pcePointwise_316 ∷ T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 → (AgdaAny → AgdaAny → T_ProofOrCE_50) → [AgdaAny] → [AgdaAny] → T_ProofOrCE_50 Source #