Documentation

Aesop.RPINF.Basic

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
              @[irreducible]

              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
                  @[irreducible]

                  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

                          An expression in PINF at transparency md.

                          Instances For
                            @[reducible, inline]

                            An expression in PINF at reducible transparency.

                            Equations
                              Instances For

                                Cache for rpinf.

                                Instances For

                                  An expression in PINF at transparency md, together with its PINF hash as computed by pinfHash.

                                  Instances For
                                    @[reducible, inline]

                                    An expression in RPINF together with its RPINF hash.

                                    Equations
                                      Instances For