def Aesop.mdataPINFIsProofName : Lean.Name

MData tag for expressions that are proofs.

Equations

• Aesop.mdataPINFIsProofName = `Aesop.pinfIsProof

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

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

Equations

• Aesop.mdataSetIsProof d = Lean.KVMap.insert d Aesop.mdataPINFIsProofName (Lean.DataValue.ofBool true)

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

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

Equations

• Aesop.mdataIsProof d = Lean.KVMap.getBool d Aesop.mdataPINFIsProofName

@[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.

Equations

• Aesop.pinfEqCore (Lean.Expr.bvar i₁) (Lean.Expr.bvar i₂) = (i₁ == i₂)
• Aesop.pinfEqCore (Lean.Expr.fvar id₁) (Lean.Expr.fvar id₂) = (id₁ == id₂)
• Aesop.pinfEqCore (Lean.Expr.mvar id₁) (Lean.Expr.mvar id₂) = (id₁ == id₂)
• Aesop.pinfEqCore (Lean.Expr.sort u) (Lean.Expr.sort v) = (u == v)
• Aesop.pinfEqCore (Lean.Expr.const n₁ us) (Lean.Expr.const n₂ vs) = (n₁ == n₂ && us == vs)
• Aesop.pinfEqCore (f₁.app e₁) (f₂.app e₂) = (Aesop.pinfEq f₁ f₂ && Aesop.pinfEq e₁ e₂)
• Aesop.pinfEqCore (Lean.Expr.lam binderName t₁ e₁ bi₁) (Lean.Expr.lam binderName_1 t₂ e₂ bi₂) = (bi₁ == bi₂ && Aesop.pinfEq t₁ t₂ && Aesop.pinfEq e₁ e₂)
• Aesop.pinfEqCore (Lean.Expr.forallE binderName t₁ e₁ bi₁) (Lean.Expr.forallE binderName_1 t₂ e₂ bi₂) = (bi₁ == bi₂ && Aesop.pinfEq t₁ t₂ && Aesop.pinfEq e₁ e₂)
• Aesop.pinfEqCore (Lean.Expr.letE declName t₁ v₁ e₁ nondep) (Lean.Expr.letE declName_1 t₂ v₂ e₂ nondep_1) = (Aesop.pinfEq v₁ v₂ && Aesop.pinfEq t₁ t₂ && Aesop.pinfEq e₁ e₂)
• Aesop.pinfEqCore (Lean.Expr.lit l₁) (Lean.Expr.lit l₂) = (l₁ == l₂)
• Aesop.pinfEqCore (Lean.Expr.proj n₁ i₁ e₁) (Lean.Expr.proj n₂ i₂ e₂) = (i₁ == i₂ && n₁ == n₂ && Aesop.pinfEq e₁ e₂)
• Aesop.pinfEqCore (Lean.Expr.mdata d e₁) x✝ = (Aesop.mdataIsProof d || Aesop.pinfEq e₁ x✝)
• Aesop.pinfEqCore x✝ (Lean.Expr.mdata d e₂) = (Aesop.mdataIsProof d || Aesop.pinfEq x✝ e₂)
• Aesop.pinfEqCore x✝¹ x✝ = false

@[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.

Equations

• Aesop.pinfEq x y = (Aesop.pinfEq.unsafe_impl_3 x y || Aesop.pinfEqCore x y)

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.

Equations

• Aesop.pinfHash e = runST fun (x : Type) => (Aesop.pinfHashCore e).run' ∅

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

An expression in PINF at transparency md.

• toExpr : Lean.Expr

def Aesop.instInhabitedPINFRaw.default {a✝ : Lean.Meta.TransparencyMode} : PINFRaw a✝

Equations

• Aesop.instInhabitedPINFRaw.default = { toExpr := default }

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

Equations

• Aesop.instInhabitedPINFRaw = { default := Aesop.instInhabitedPINFRaw.default }

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

Equations

• Aesop.instBEqPINFRaw = { beq := fun (x y : Aesop.PINFRaw md) => Aesop.pinfEq x.toExpr y.toExpr }

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

Equations

• Aesop.instHashablePINFRaw = { hash := fun (x : Aesop.PINFRaw md) => Aesop.pinfHash x.toExpr }

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

Equations

• Aesop.instToStringPINFRaw = { toString := fun (x : Aesop.PINFRaw md) => toString x.toExpr }

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

Equations

• Aesop.instToFormatPINFRaw = { format := fun (x : Aesop.PINFRaw md) => Std.format x.toExpr }

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

Equations

• Aesop.instToMessageDataPINFRaw = { toMessageData := fun (x : Aesop.PINFRaw md) => Lean.toMessageData x.toExpr }

@[reducible, inline]

abbrev Aesop.RPINFRaw : Type

An expression in PINF at reducible transparency.

Equations

• Aesop.RPINFRaw = Aesop.PINFRaw Lean.Meta.TransparencyMode.reducible

structure Aesop.RPINFCache : Type

Cache for rpinf.

• map : Std.HashMap Lean.Expr RPINFRaw

def Aesop.instInhabitedRPINFCache.default : RPINFCache

Equations

• Aesop.instInhabitedRPINFCache.default = { map := default }

instance Aesop.instInhabitedRPINFCache : Inhabited RPINFCache

Equations

• Aesop.instInhabitedRPINFCache = { default := Aesop.instInhabitedRPINFCache.default }

instance Aesop.instEmptyCollectionRPINFCache : EmptyCollection RPINFCache

Equations

• Aesop.instEmptyCollectionRPINFCache = { emptyCollection := { map := ∅ } }

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✝)

Equations

• Aesop.instInhabitedPINF = { default := Aesop.instInhabitedPINF.default }

def Aesop.instInhabitedPINF.default {a✝ : Lean.Meta.TransparencyMode} : PINF a✝

Equations

• Aesop.instInhabitedPINF.default = { toExpr := default, hash := default }

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

Equations

• Aesop.instBEqPINF = { beq := fun (x y : Aesop.PINF md) => Aesop.pinfEq x.toExpr y.toExpr }

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

Equations

• Aesop.instHashablePINF = { hash := fun (x : Aesop.PINF md) => x.hash }

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

Equations

• Aesop.instOrdPINF = { compare := fun (x y : Aesop.PINF md) => if (x == y) = true then Ordering.eq else if x.toExpr.lt y.toExpr = true then Ordering.lt else Ordering.gt }

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

Equations

• Aesop.instToStringPINF = { toString := fun (x : Aesop.PINF md) => toString x.toExpr }

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

Equations

• Aesop.instToFormatPINF = { format := fun (x : Aesop.PINF md) => Std.format x.toExpr }

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

Equations

• Aesop.instToMessageDataPINF = { toMessageData := fun (x : Aesop.PINF md) => Lean.toMessageData x.toExpr }

@[reducible, inline]

abbrev Aesop.RPINF : Type

An expression in RPINF together with its RPINF hash.

Equations

• Aesop.RPINF = Aesop.PINF Lean.Meta.TransparencyMode.reducible