source
def Aesop.mdataPINFIsProofName :
Lean.Name

`MData` tag for expressions that are proofs.

Equations

- Aesop.mdataPINFIsProofName = `Aesop.pinfIsProof

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
@[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)

Instances For

source
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`.

source
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' ∅

Instances For

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

An expression in PINF at transparency `md`.

- toExpr : Lean.Expr

Instances For

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

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

Instances For

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

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

source
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 }

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

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

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

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

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

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

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

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

source
@[reducible, inline]
abbrev Aesop.RPINFRaw :
Type

An expression in PINF at `reducible` transparency.

Equations

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

Instances For

source
structure Aesop.RPINFCache :
Type

Cache for `rpinf`.

- map : Std.HashMap Lean.Expr RPINFRaw

Instances For

source
instance Aesop.instInhabitedRPINFCache :
Inhabited RPINFCache
Equations

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

source
def Aesop.instInhabitedRPINFCache.default :
RPINFCache
Equations

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

Instances For

source
instance Aesop.instEmptyCollectionRPINFCache :
EmptyCollection RPINFCache
Equations

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

source
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

Instances For

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

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

Instances For

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

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

source
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 }

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

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

source
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 }

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

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

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

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

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

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

source
@[reducible, inline]
abbrev Aesop.RPINF :
Type

An expression in RPINF together with its RPINF hash.

Equations

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

Instances For