@[reducible, inline]

abbrev Duper.ExprPos : Type

Positions in an expression: Counting argument numbers from the right e.g. a is at #[1] and b is at #[0] in f a b. If the head is an implication (an expression of the form ∀ _ : p, q where p and q have type Prop) then we treat p and q as arguments passed to a hypothetical implication symbol.

Equations

• Duper.ExprPos = Array Nat

def Duper.ExprPos.empty : ExprPos

Equations

• Duper.ExprPos.empty = #[]

@[inline]

def Lean.Expr.hasAnyMVar (e : Expr) (p : MVarId → Bool) : Bool

Return true iff e contains an mvar which satisfies p. This is adapted from Lean.Expr.hasAnyFVar

Equations

• e.hasAnyMVar p = Lean.Expr.hasAnyMVar.visit p e

@[specialize #[]]

def Lean.Expr.hasAnyMVar.visit (p : MVarId → Bool) (e : Expr) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Expr.hasAnyMVar.visit p (Lean.Expr.mdata data e_2) = if (!(Lean.Expr.mdata data e_2).hasMVar) = true then false else Lean.Expr.hasAnyMVar.visit p e_2
• Lean.Expr.hasAnyMVar.visit p (f.app a) = if (!(f.app a).hasMVar) = true then false else Lean.Expr.hasAnyMVar.visit p f || Lean.Expr.hasAnyMVar.visit p a
• Lean.Expr.hasAnyMVar.visit p (Lean.Expr.proj typeName idx e_2) = if (!(Lean.Expr.proj typeName idx e_2).hasMVar) = true then false else Lean.Expr.hasAnyMVar.visit p e_2
• Lean.Expr.hasAnyMVar.visit p (Lean.Expr.mvar mvarId) = if (!(Lean.Expr.mvar mvarId).hasMVar) = true then false else p mvarId
• Lean.Expr.hasAnyMVar.visit p e = if (!e.hasMVar) = true then false else false

def Lean.Expr.isMVar' (e : Expr) : Bool

This should be used in place of Lean.Expr.isMVar so that mvars surrounded by mdata are not missed.

Equations

• e.isMVar' = e.consumeMData.isMVar

def Lean.Expr.impAwareGetAppRevArgs (e : Expr) : MetaM (Array Expr)

Same as Lean.Expr.getAppRevArgs but if the head is an implication (an expression of the form ∀ _ : p, q where p and q have type Prop), then it pretends the head has the form .app (.app impSymbol p) q

Equations

• e.impAwareGetAppRevArgs = Lean.Expr.impAwareGetAppRevArgsAux✝ e (Array.mkEmpty e.getAppNumArgs)

def Lean.Expr.impAwareGetAppArgs (e : Expr) : MetaM (Array Expr)

Same as Lean.Expr.getAppArgs but if the head is an implication (an expression of the form ∀ _ : p, q where p and q have type Prop), then it pretends the head has the form .app (.app impSymbol p) q

Equations

• e.impAwareGetAppArgs = do let revArgs ← e.impAwareGetAppRevArgs pure revArgs.reverse

def Lean.Expr.impAwareGetRevArg! : Expr → Nat → Expr

Note: This function assumes that if the head is a forallE expression and the index given indicates either the type or body of the forallE expression, then the head is actually an implication (in other words, this function does not check whether the head a valid implication as opposed to an arbitrary forallE expression)

Equations

• One or more equations did not get rendered due to their size.
• (fn.app a).impAwareGetRevArg! 0 = a
• (f.app arg).impAwareGetRevArg! i.succ = f.impAwareGetRevArg! i
• (Lean.Expr.forallE binderName binderType b binderInfo).impAwareGetRevArg! 0 = b
• (Lean.Expr.forallE binderName t body binderInfo).impAwareGetRevArg! 1 = t

partial def Lean.Expr.foldGreenM {m : Type → Type u_1} {β : Type} [Monad m] [MonadLiftT MetaM m] (f : β → Expr → Duper.ExprPos → m β) (init : β) (e : Expr) (pos : Duper.ExprPos := Duper.ExprPos.empty) : optParam (Inhabited β) { default := init } → m β

def Lean.Expr.getAtPos! {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : Duper.ExprPos) : m Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Expr.getAtPos? {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : Duper.ExprPos) : m (Option Expr)

Returns the expression in e indiced by pos if it exists, and returns none if pos does not point to a valid subexpression in e

Equations

• One or more equations did not get rendered due to their size.

def Lean.Expr.getAtUntypedPos {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : Duper.ExprPos) : m (Option Expr)

"Untyped" positions are positions on potentially ill-typed expressions produced by the ⌊e⌋ function described in https://matryoshka-project.github.io/pubs/hounif_article.pdf and implemented in Fingerprint.lean's transformToUntypedFirstOrderTerm. Untyped positions are not intended to be consistent with ordinary expression positions, both because of the transformations performed by the ⌊e⌋ function, and because we cannot distinguish implications from arbitrary forallE expressions in potentially ill-typed expressions. Consequently, this function should only be used internally by Fingerprint.lean.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Expr.canInstantiateToGetAtPos {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : Duper.ExprPos) (startIndex : Nat := 0) : m Bool

Returns true if either the subexpression indiced by pos exists in e, or if it may be possible to instantiate metavariables in e in such a way that the subexpression indiced by pos would exist.

For example, if e = "f 2 ?m.0", then canInstantiateToGetAtPos would return true for pos #[0, 1] (becuase "?m.0" could be instantiated as an application) but would return false for pos #[1, 1] (because 2 does not and can not have any arguments)

partial def Lean.Expr.canInstantiateToGetAtUntypedPos (e : Expr) (pos : Duper.ExprPos) (startIndex : Nat := 0) : Bool

partial def Lean.Expr.getTopSymbol (e : Expr) : Expr

def Lean.Expr.replaceAtPos? {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : Duper.ExprPos) (replacement : Expr) : m (Option Expr)

Attempts to put replacement at pos in e. Returns some res if successful, and returns none otherwise

Equations

• e.replaceAtPos? pos replacement = Lean.Expr.replaceAtPosHelper✝ e pos.toList replacement

def Lean.Expr.replaceAtPos! {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : Duper.ExprPos) (replacement : Expr) : m Expr

Attempts to put replacement at pos in e. Returns the result if successful and throws and error otherwise

Equations

• One or more equations did not get rendered due to their size.

def Lean.Expr.replaceGreenWithPos {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (t₁ t₂ e : Expr) : m (Expr × Array Duper.ExprPos)

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Expr.replaceWithPos (t₁ t₂ e : Expr) : Expr

def Lean.Expr.abstractAtPos! {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : Duper.ExprPos) : m Expr

This function acts as Meta.kabstract except that it takes an ExprPos rather than Occurrences and expects the given expression to consist only of applications up to the given ExprPos. Additionally, since the exact ExprPos is given, we don't need to pass in Meta.kabstract's second argument p

Equations

• e.abstractAtPos! pos = Lean.Expr.abstractAtPosHelper!✝ e pos.toList 0

def Lean.Expr.abstractAtPoses! {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (poses : Array Duper.ExprPos) : m Expr

Equations

• e.abstractAtPoses! poses = Lean.Expr.abstractAtPosesHelper!✝ e (Array.map (fun (x : Duper.ExprPos) => x.toList) poses) 0

def Lean.Expr.weight : Expr → Nat

Equations

• (Lean.Expr.bvar deBruijnIndex).weight = 1
• (Lean.Expr.fvar fvarId).weight = 1
• (Lean.Expr.mvar mvarId).weight = 1
• (Lean.Expr.sort u).weight = 1
• (Lean.Expr.const declName us).weight = 1
• (a.app b).weight = a.weight + b.weight
• (Lean.Expr.lam binderName binderType b binderInfo).weight = 1 + b.weight
• (Lean.Expr.forallE binderName binderType b binderInfo).weight = 1 + b.weight
• (Lean.Expr.letE declName type v b nonDep).weight = 1 + v.weight + b.weight
• (Lean.Expr.lit a).weight = 1
• (Lean.Expr.mdata data b).weight = 1 + b.weight
• (Lean.Expr.proj typeName idx b).weight = 1 + b.weight

def Lean.Expr.expressionsAgreeExceptAtPos {m : Type → Type u_1} [Monad m] [MonadLiftT MetaM m] (e1 e2 : Expr) (p : Duper.ExprPos) : m Bool

Returns true iff e1 and e2 are identical except potentially at position p. Returns false if p is not a valid position for either e1 or e2.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Expr.isFullyAppliedLogicalSymbol (e : Expr) : Bool

Returns true iff e is a fully applied logical symbol. The set of symbols we consider to be logical symbols are: ∧, ∨, →, ↔, ¬, True, False, ∀, ∃, =, and ≠

Equations

• One or more equations did not get rendered due to their size.