MData
tag for expressions that are proofs.
Equations
Instances For
Modify d
to indicate that the enclosed expression is a proof.
Equations
Instances For
Check whether d
indicates that the enclosed expression is a proof.
Equations
Instances For
Check whether two expressions in PINF are equal. We assume that the two expressions are type-correct, in PINF and have defeq types.
Equations
Instances For
Check whether two expressions in PINF are equal. We assume that the two expressions are type-correct, in PINF and have defeq types.
Equations
Instances For
Compute the PINF hash of an expression in PINF. The hash ignores binder
names, binder info and proofs marked by mdataPINFIsProofName
.
Compute the PINF hash of an expression in PINF. The hash ignores binder
names, binder info and proofs marked by mdataPINFIsProofName
.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
An expression in PINF at reducible
transparency.
Equations
Instances For
An expression in PINF at transparency md
, together with its PINF hash as
computed by pinfHash
.
Instances For
Equations
Equations
Equations
Equations
Equations
An expression in RPINF together with its RPINF hash.