def Aesop.mdataPINFIsProofName : Lean.Name

MData tag for expressions that are proofs.

def Aesop.mdataSetIsProof (d : Lean.MData) : Lean.MData

Modify d to indicate that the enclosed expression is a proof.

def Aesop.mdataIsProof (d : Lean.MData) : Bool

Check whether d indicates that the enclosed expression is a proof.

@[irreducible]

def Aesop.pinfEqCore (x y : Lean.Expr) : Bool

Check whether two expressions in PINF are equal. We assume that the two expressions are type-correct, in PINF and have defeq types.

@[irreducible]

def Aesop.pinfEq (x y : Lean.Expr) : Bool

Check whether two expressions in PINF are equal. We assume that the two expressions are type-correct, in PINF and have defeq types.

partial def Aesop.pinfHashCore {s : Type} (e : Lean.Expr) : StateRefT' s (Std.HashMap UInt64 UInt64) (ST s) UInt64

Compute the PINF hash of an expression in PINF. The hash ignores binder names, binder info and proofs marked by mdataPINFIsProofName.

def Aesop.pinfHash (e : Lean.Expr) : UInt64

Compute the PINF hash of an expression in PINF. The hash ignores binder names, binder info and proofs marked by mdataPINFIsProofName.

structure Aesop.PINFRaw (md : Lean.Meta.TransparencyMode) : Type

An expression in PINF at transparency md.

• toExpr : Lean.Expr

instance Aesop.instInhabitedPINFRaw {a✝ : Lean.Meta.TransparencyMode} : Inhabited (PINFRaw a✝)

instance Aesop.instBEqPINFRaw {md : Lean.Meta.TransparencyMode} : BEq (PINFRaw md)

instance Aesop.instHashablePINFRaw {md : Lean.Meta.TransparencyMode} : Hashable (PINFRaw md)

instance Aesop.instToStringPINFRaw {md : Lean.Meta.TransparencyMode} : ToString (PINFRaw md)

instance Aesop.instToFormatPINFRaw {md : Lean.Meta.TransparencyMode} : Std.ToFormat (PINFRaw md)

instance Aesop.instToMessageDataPINFRaw {md : Lean.Meta.TransparencyMode} : Lean.ToMessageData (PINFRaw md)

@[reducible, inline]

abbrev Aesop.RPINFRaw : Type

An expression in PINF at reducible transparency.

structure Aesop.RPINFCache : Type

Cache for rpinf.

• map : Std.HashMap Lean.Expr RPINFRaw

instance Aesop.instInhabitedRPINFCache : Inhabited RPINFCache

instance Aesop.instEmptyCollectionRPINFCache : EmptyCollection RPINFCache

structure Aesop.PINF (md : Lean.Meta.TransparencyMode) : Type

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

• toExpr : Lean.Expr
• hash : UInt64

instance Aesop.instInhabitedPINF {a✝ : Lean.Meta.TransparencyMode} : Inhabited (PINF a✝)

instance Aesop.instBEqPINF {md : Lean.Meta.TransparencyMode} : BEq (PINF md)

instance Aesop.instHashablePINF {md : Lean.Meta.TransparencyMode} : Hashable (PINF md)

instance Aesop.instOrdPINF {md : Lean.Meta.TransparencyMode} : Ord (PINF md)

instance Aesop.instToStringPINF {md : Lean.Meta.TransparencyMode} : ToString (PINF md)

instance Aesop.instToFormatPINF {md : Lean.Meta.TransparencyMode} : Std.ToFormat (PINF md)

instance Aesop.instToMessageDataPINF {md : Lean.Meta.TransparencyMode} : Lean.ToMessageData (PINF md)

@[reducible, inline]

abbrev Aesop.RPINF : Type

An expression in RPINF together with its RPINF hash.