Documentation

Inhabited Lean.BinderInfo

instance Lean.instInhabitedBinderInfo :

Equations

Lean.instInhabitedBinderInfo = { default := Lean.BinderInfo.default }

instance Lean.instBEqBinderInfo :

BEq Lean.BinderInfo

Equations

Lean.instBEqBinderInfo = { beq := Lean.beqBinderInfo✝ }

instance Lean.instReprBinderInfo :

Repr Lean.BinderInfo

Equations

Lean.instReprBinderInfo = { reprPrec := Lean.reprBinderInfo✝ }

def Lean.BinderInfo.hash :

Lean.BinderInfo → UInt64

Equations

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

def Lean.BinderInfo.isExplicit :

Return true if the given BinderInfo does not correspond to an implicit binder annotation (i.e., implicit, strictImplicit, or instImplicit).

Equations

Lean.BinderInfo.isExplicit x = match x with | Lean.BinderInfo.implicit => false | Lean.BinderInfo.strictImplicit => false | Lean.BinderInfo.instImplicit => false | x => true

instance Lean.instHashableBinderInfo :

Hashable Lean.BinderInfo

Equations

Lean.instHashableBinderInfo = { hash := Lean.BinderInfo.hash }

def Lean.BinderInfo.isInstImplicit :

Return true if the given BinderInfo is an instance implicit annotation (e.g., [Decidable α])

Equations

Lean.BinderInfo.isInstImplicit x = match x with | Lean.BinderInfo.instImplicit => true | x => false

def Lean.BinderInfo.isImplicit :

Return true if the given BinderInfo is a regular implicit annotation (e.g., {α : Type u})

Equations

Lean.BinderInfo.isImplicit x = match x with | Lean.BinderInfo.implicit => true | x => false

def Lean.BinderInfo.isStrictImplicit :

Return true if the given BinderInfo is a strict implicit annotation (e.g., {{α : Type u}})

Equations

Lean.BinderInfo.isStrictImplicit x = match x with | Lean.BinderInfo.strictImplicit => true | x => false

@[inline]

abbrev Lean.MData :

Expression metadata. Used with the Expr.mdata constructor.

Equations

Lean.MData = Lean.KVMap

@[inline]

abbrev Lean.MData.empty :

Lean.MData

Equations

Lean.MData.empty = { entries := [] }

def Lean.Expr.Data :

Cached hash code, cached results, and other data for Expr.

hash : 32-bits
approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
hasFVar : 1-bit -- does it contain free variables?
hasExprMVar : 1-bit -- does it contain metavariables?
hasLevelMVar : 1-bit -- does it contain level metavariables?
hasLevelParam : 1-bit -- does it contain level parameters?
looseBVarRange : 20-bits

Remark: this is mostly an internal datastructure used to implement Expr, most will never have to use it.

Equations

Lean.Expr.Data = UInt64

instance Lean.instInhabitedData_1 :

Inhabited Lean.Expr.Data

Equations

Lean.instInhabitedData_1 = inferInstanceAs (Inhabited UInt64)

def Lean.Expr.Data.hash (c : Lean.Expr.Data) :

UInt64

Equations

Lean.Expr.Data.hash c = UInt32.toUInt64 (UInt64.toUInt32 c)

instance Lean.instBEqData_1 :

BEq Lean.Expr.Data

Equations

Lean.instBEqData_1 = { beq := fun a b => a == b }

def Lean.Expr.Data.approxDepth (c : Lean.Expr.Data) :

UInt8

Equations

Lean.Expr.Data.approxDepth c = UInt64.toUInt8 (UInt64.land (UInt64.shiftRight c 32) 255)

def Lean.Expr.Data.looseBVarRange (c : Lean.Expr.Data) :

UInt32

Equations

Lean.Expr.Data.looseBVarRange c = UInt64.toUInt32 (UInt64.shiftRight c 44)

def Lean.Expr.Data.hasFVar (c : Lean.Expr.Data) :

Equations

Lean.Expr.Data.hasFVar c = (UInt64.land (UInt64.shiftRight c 40) 1 == 1)

def Lean.Expr.Data.hasExprMVar (c : Lean.Expr.Data) :

Equations

Lean.Expr.Data.hasExprMVar c = (UInt64.land (UInt64.shiftRight c 41) 1 == 1)

def Lean.Expr.Data.hasLevelMVar (c : Lean.Expr.Data) :

Equations

Lean.Expr.Data.hasLevelMVar c = (UInt64.land (UInt64.shiftRight c 42) 1 == 1)

def Lean.Expr.Data.hasLevelParam (c : Lean.Expr.Data) :

Equations

Lean.Expr.Data.hasLevelParam c = (UInt64.land (UInt64.shiftRight c 43) 1 == 1)

@[extern c inline "(uint64_t)#1"]

def Lean.BinderInfo.toUInt64 :

Lean.BinderInfo → UInt64

Equations

Lean.BinderInfo.toUInt64 x = match x with | Lean.BinderInfo.default => 0 | Lean.BinderInfo.implicit => 1 | Lean.BinderInfo.strictImplicit => 2 | Lean.BinderInfo.instImplicit => 3

def Lean.Expr.mkData (h : UInt64) (looseBVarRange : optParam Nat 0) (approxDepth : optParam UInt32 0) (hasFVar : optParam Bool false) (hasExprMVar : optParam Bool false) (hasLevelMVar : optParam Bool false) (hasLevelParam : optParam Bool false) :

Equations

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

@[inline]

def Lean.Expr.mkAppData (fData : Lean.Expr.Data) (aData : Lean.Expr.Data) :

Optimized version of Expr.mkData for applications.

Equations

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

@[inline]

def Lean.Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar : Bool) (hasExprMVar : Bool) (hasLevelMVar : Bool) (hasLevelParam : Bool) :

Equations

Lean.Expr.mkDataForBinder h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

@[inline]

def Lean.Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar : Bool) (hasExprMVar : Bool) (hasLevelMVar : Bool) (hasLevelParam : Bool) :

Equations

Lean.Expr.mkDataForLet h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

instance Lean.instReprData_1 :

Repr Lean.Expr.Data

Equations

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

structure Lean.FVarId :

name : Lean.Name

The unique free variable identifier. It is just a hierarchical name, but we wrap it in FVarId to make sure they don't get mixed up with MVarId.

This is not the user-facing name for a free variable. This information is stored in the local context (LocalContext). The unique identifiers are generated using a NameGenerator.

Instances For

instance Lean.instInhabitedFVarId :

Inhabited Lean.FVarId

Equations

Lean.instInhabitedFVarId = { default := { name := default } }

instance Lean.instBEqFVarId :

BEq Lean.FVarId

Equations

Lean.instBEqFVarId = { beq := Lean.beqFVarId✝ }

instance Lean.instHashableFVarId :

Hashable Lean.FVarId

Equations

Lean.instHashableFVarId = { hash := Lean.hashFVarId✝ }

instance Lean.instReprFVarId :

Repr Lean.FVarId

Equations

Lean.instReprFVarId = { reprPrec := fun n p => reprPrec n.name p }

def Lean.FVarIdSet :

A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees.

Equations

Lean.FVarIdSet = Lean.RBTree Lean.FVarId fun x x_1 => Lean.Name.quickCmp x.name x_1.name

instance Lean.instForInFVarIdSetFVarId {m : Type u_1 → Type u_2} :

ForIn m Lean.FVarIdSet Lean.FVarId

Equations

Lean.instForInFVarIdSetFVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.FVarId fun x x_1 => Lean.Name.quickCmp x.name x_1.name) Lean.FVarId)

def Lean.FVarIdSet.insert (s : Lean.FVarIdSet) (fvarId : Lean.FVarId) :

Lean.FVarIdSet

Equations

Lean.FVarIdSet.insert s fvarId = Lean.RBTree.insert s fvarId

def Lean.FVarIdHashSet :

A set of unique free variable identifiers implemented using hashtables. Hashtables are faster than red-black trees if they are used linearly. They are not persistent data-structures.

Equations

Lean.FVarIdHashSet = Lean.HashSet Lean.FVarId

def Lean.FVarIdMap (α : Type) :

A mapping from free variable identifiers to values of type α. This is a persistent data structure implemented using red-black trees.

Equations

Lean.FVarIdMap α = Lean.RBMap Lean.FVarId α fun x x_1 => Lean.Name.quickCmp x.name x_1.name

def Lean.FVarIdMap.insert {α : Type} (s : Lean.FVarIdMap α) (fvarId : Lean.FVarId) (a : α) :

Lean.FVarIdMap α

Equations

Lean.FVarIdMap.insert s fvarId a = Lean.RBMap.insert s fvarId a

instance Lean.instEmptyCollectionFVarIdMap {α : Type} :

EmptyCollection (Lean.FVarIdMap α)

Equations

Lean.instEmptyCollectionFVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.FVarId α fun x x_1 => Lean.Name.quickCmp x.name x_1.name))

instance Lean.instInhabitedFVarIdMap {α : Type} :

Inhabited (Lean.FVarIdMap α)

Equations

Lean.instInhabitedFVarIdMap = { default := ∅ }

structure Lean.MVarId :

name : Lean.Name

Universe metavariable Id

Instances For

instance Lean.instInhabitedMVarId :

Inhabited Lean.MVarId

Equations

Lean.instInhabitedMVarId = { default := { name := default } }

instance Lean.instBEqMVarId :

BEq Lean.MVarId

Equations

Lean.instBEqMVarId = { beq := Lean.beqMVarId✝ }

instance Lean.instHashableMVarId :

Hashable Lean.MVarId

Equations

Lean.instHashableMVarId = { hash := Lean.hashMVarId✝ }

instance Lean.instReprMVarId :

Repr Lean.MVarId

Equations

Lean.instReprMVarId = { reprPrec := Lean.reprMVarId✝ }

instance Lean.instReprMVarId_1 :

Repr Lean.MVarId

Equations

Lean.instReprMVarId_1 = { reprPrec := fun n p => reprPrec n.name p }

def Lean.MVarIdSet :

Equations

Lean.MVarIdSet = Lean.RBTree Lean.MVarId fun x x_1 => Lean.Name.quickCmp x.name x_1.name

def Lean.MVarIdSet.insert (s : Lean.MVarIdSet) (mvarId : Lean.MVarId) :

Lean.MVarIdSet

Equations

Lean.MVarIdSet.insert s mvarId = Lean.RBTree.insert s mvarId

instance Lean.instForInMVarIdSetMVarId {m : Type u_1 → Type u_2} :

ForIn m Lean.MVarIdSet Lean.MVarId

Equations

Lean.instForInMVarIdSetMVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.MVarId fun x x_1 => Lean.Name.quickCmp x.name x_1.name) Lean.MVarId)

def Lean.MVarIdMap (α : Type) :

Equations

Lean.MVarIdMap α = Lean.RBMap Lean.MVarId α fun x x_1 => Lean.Name.quickCmp x.name x_1.name

def Lean.MVarIdMap.insert {α : Type} (s : Lean.MVarIdMap α) (mvarId : Lean.MVarId) (a : α) :

Lean.MVarIdMap α

Equations

Lean.MVarIdMap.insert s mvarId a = Lean.RBMap.insert s mvarId a

instance Lean.instEmptyCollectionMVarIdMap {α : Type} :

EmptyCollection (Lean.MVarIdMap α)

Equations

Lean.instEmptyCollectionMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.MVarId α fun x x_1 => Lean.Name.quickCmp x.name x_1.name))

instance Lean.instForInMVarIdMapProdMVarId {m : Type u_1 → Type u_2} {α : Type} :

ForIn m (Lean.MVarIdMap α) (Lean.MVarId × α)

Equations

Lean.instForInMVarIdMapProdMVarId = inferInstanceAs (ForIn m (Lean.RBMap Lean.MVarId α fun x x_1 => Lean.Name.quickCmp x.name x_1.name) (Lean.MVarId × α))

instance Lean.instInhabitedMVarIdMap {α : Type} :

Inhabited (Lean.MVarIdMap α)

Equations

Lean.instInhabitedMVarIdMap = { default := ∅ }

@[extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]

noncomputable def Lean.Expr.data :

Lean.Expr → Lean.Expr.Data

inductive Lean.Expr :

The bvar constructor represents bound variables, i.e. occurrences of a variable in the expression where there is a variable binder above it (i.e. introduced by a lam, forallE, or letE).
The deBruijnIndex parameter is the de-Bruijn index for the bound variable. See here for additional information on de-Bruijn indexes.
For example, consider the expression fun x : Nat => forall y : Nat, x = y. The x and y variables in the equality expression are constructed using bvar and bound to the binders introduced by the earlier lam and forallE constructors. Here is the corresponding Expr representation for the same expression:
```
.lam `x (.const `Nat [])
  (.forallE `y (.const `Nat [])
    (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0))
    .default)
  .default
```
bvar: Nat → Lean.Expr
The fvar constructor represent free variables. These /free/ variable occurrences are not bound by an earlier lam, forallE, or letE contructor and its binder exists in a local context only.
Note that Lean uses the /locally nameless approach/. See here for additional details.
When "visiting" the body of a binding expression (i.e. lam, forallE, or letE), bound variables are converted into free variables using a unique identifier, and their user-facing name, type, value (for LetE), and binder annotation are stored in the LocalContext.
fvar: Lean.FVarId → Lean.Expr
Metavariables are used to represent "holes" in expressions, and goals in the tactic framework. Metavariable declarations are stored in the MetavarContext. Metavariables are used during elaboration, and are not allowed in the kernel, or in the code generator.
mvar: Lean.MVarId → Lean.Expr
Used for Type u, Sort u, and Prop:
- Prop is represented as .sort .zero,
- Sort u as .sort (.param `u), and
- Type u as .sort (.succ (.param `u))
sort: Lean.Level → Lean.Expr
A (universe polymorphic) constant that has been defined earlier in the module or by another imported module. For example, @Eq.{1} is represented as Expr.const `Eq [.succ .zero], and @Array.map.{0, 0} is represented as Expr.const `Array.map [.zero, .zero].
const: Lean.Name → List Lean.Level → Lean.Expr
A function application.
For example, the natural number one, i.e. Nat.succ Nat.zero is represented as Expr.app (.const Nat.succ []) (.const .zero [])` Note that multiple arguments are represented using partial application.
For example, the two argument application f x y is represented as Expr.app (.app f x) y.
app: Lean.Expr → Lean.Expr → Lean.Expr
A lambda abstraction (aka anonymous functions). It introduces a new binder for variable x in scope for the lambda body.
For example, the expression fun x : Nat => x is represented as
```
Expr.lam `x (.const `Nat []) (.bvar 0) .default
```
lam: Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
A dependent arrow (a : α) → β) (aka forall-expression) where β may dependent on a. Note that this constructor is also used to represent non-dependent arrows where β does not depend on a.
For example:
- forall x : Prop, x ∧ x:
```
Expr.forallE `x (.sort .zero)
  (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
```
- Nat → Bool:
```
Expr.forallE `a (.const `Nat [])
  (.const `Bool []) .default
```
forallE: Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
Let-expressions.
IMPORTANT: The nonDep flag is for "local" use only. That is, a module should not "trust" its value for any purpose. In the intended use-case, the compiler will set this flag, and be responsible for maintaining it. Other modules may not preserve its value while applying transformations.
Given an environment, a metavariable context, and a local context, we say a let-expression let x : t := v; e is non-dependent when it is equivalent to (fun x : t => e) v. Here is an example of a dependent let-expression let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b is type correct, but (fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2 is not.
The let-expression let x : Nat := 2; Nat.succ x is represented as
```
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
letE: Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
Natural number and string literal values.
They are not really needed, but provide a more compact representation in memory for these two kinds of literals, and are used to implement efficient reduction in the elaborator and kernel. The "raw" natural number 2 can be represented as Expr.lit (.natVal 2). Note that, it is definitionally equal to:
```
Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
lit: Lean.Literal → Lean.Expr
Metadata (aka annotations).
We use annotations to provide hints to the pretty-printer, store references to Syntax nodes, position information, and save information for elaboration procedures (e.g., we use the inaccessible annotation during elaboration to mark Exprs that correspond to inaccessible patterns).
Note that Expr.mdata data e is definitionally equal to e.
mdata: Lean.MData → Lean.Expr → Lean.Expr
Projection-expressions. They are redundant, but are used to create more compact terms, speedup reduction, and implement eta for structures. The type of struct must be an structure-like inductive type. That is, it has only one constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators check whether the typeName matches the type of struct, and whether the (zero-based) index is valid (i.e., it is smaller than the numbef of constructor fields). When exporting Lean developments to other systems, proj can be replaced with typeName.rec applications.
Example, given a : Nat x Bool, a.1 is represented as
```
.proj `Prod 0 a
```
proj: Lean.Name → Nat → Lean.Expr → Lean.Expr

Lean expressions. This data structure is used in the kernel and elaborator. However, expressions sent to the kernel should not contain metavariables.

Remark: we use the E suffix (short for Expr) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use.

Instances For

instance Lean.instInhabitedExpr :

Inhabited Lean.Expr

Equations

Lean.instInhabitedExpr = { default := Lean.Expr.bvar default }

instance Lean.instReprExpr :

Repr Lean.Expr

Equations

Lean.instReprExpr = { reprPrec := Lean.reprExpr✝ }

def Lean.Expr.ctorName :

Lean.Expr → String

The constructor name for the given expression. This is used for debugging purposes.

Equations

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

def Lean.Expr.hash (e : Lean.Expr) :

UInt64

Equations

Lean.Expr.hash e = Lean.Expr.Data.hash (Lean.Expr.data e)

instance Lean.Expr.instHashableExpr :

Hashable Lean.Expr

Equations

Lean.Expr.instHashableExpr = { hash := Lean.Expr.hash }

def Lean.Expr.hasFVar (e : Lean.Expr) :

Return true if e contains free variables. This is a constant time operation.

Equations

Lean.Expr.hasFVar e = Lean.Expr.Data.hasFVar (Lean.Expr.data e)

def Lean.Expr.hasExprMVar (e : Lean.Expr) :

Return true if e contains expression metavariables. This is a constant time operation.

Equations

Lean.Expr.hasExprMVar e = Lean.Expr.Data.hasExprMVar (Lean.Expr.data e)

def Lean.Expr.hasLevelMVar (e : Lean.Expr) :

Return true if e contains universe (aka Level) metavariables. This is a constant time operation.

Equations

Lean.Expr.hasLevelMVar e = Lean.Expr.Data.hasLevelMVar (Lean.Expr.data e)

def Lean.Expr.hasMVar (e : Lean.Expr) :

Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.

Equations

Lean.Expr.hasMVar e = let d := Lean.Expr.data e; Lean.Expr.Data.hasExprMVar d || Lean.Expr.Data.hasLevelMVar d

def Lean.Expr.hasLevelParam (e : Lean.Expr) :

Return true if e contains universe level parameters. This is a constant time operation.

Equations

Lean.Expr.hasLevelParam e = Lean.Expr.Data.hasLevelParam (Lean.Expr.data e)

def Lean.Expr.approxDepth (e : Lean.Expr) :

UInt32

Return the approximated depth of an expression. This information is used to compute the expression hash code, and speedup comparisons. This is a constant time operation. We say it is approximate because it maxes out at 255.

Equations

Lean.Expr.approxDepth e = UInt8.toUInt32 (Lean.Expr.Data.approxDepth (Lean.Expr.data e))

def Lean.Expr.looseBVarRange (e : Lean.Expr) :

Nat

The range of de-Bruijn variables that are loose. That is, bvars that are not bound by a binder. For example, bvar i has range i + 1 and an expression with no loose bvars has range 0.

Equations

Lean.Expr.looseBVarRange e = UInt32.toNat (Lean.Expr.Data.looseBVarRange (Lean.Expr.data e))

def Lean.Expr.binderInfo (e : Lean.Expr) :

Lean.BinderInfo

Return the binder information if e is a lambda or forall expression, and .default otherwise.

Equations

Lean.Expr.binderInfo e = match e with | Lean.Expr.forallE binderName binderType body bi => bi | Lean.Expr.lam binderName binderType body bi => bi | x => Lean.BinderInfo.default

Export functions.

@[export lean_expr_hash]

def Lean.Expr.hashEx :

Lean.Expr → UInt64

Equations

Lean.Expr.hashEx = hash

@[export lean_expr_has_fvar]

def Lean.Expr.hasFVarEx :

Equations

Lean.Expr.hasFVarEx = Lean.Expr.hasFVar

@[export lean_expr_has_expr_mvar]

def Lean.Expr.hasExprMVarEx :

Equations

Lean.Expr.hasExprMVarEx = Lean.Expr.hasExprMVar

@[export lean_expr_has_level_mvar]

def Lean.Expr.hasLevelMVarEx :

Equations

Lean.Expr.hasLevelMVarEx = Lean.Expr.hasLevelMVar

@[export lean_expr_has_mvar]

def Lean.Expr.hasMVarEx :

Equations

Lean.Expr.hasMVarEx = Lean.Expr.hasMVar

@[export lean_expr_has_level_param]

def Lean.Expr.hasLevelParamEx :

Equations

Lean.Expr.hasLevelParamEx = Lean.Expr.hasLevelParam

@[export lean_expr_loose_bvar_range]

def Lean.Expr.looseBVarRangeEx (e : Lean.Expr) :

UInt32

Equations

Lean.Expr.looseBVarRangeEx e = Lean.Expr.Data.looseBVarRange (Lean.Expr.data e)

@[export lean_expr_binder_info]

def Lean.Expr.binderInfoEx :

Lean.Expr → Lean.BinderInfo

Equations

Lean.Expr.binderInfoEx = Lean.Expr.binderInfo

def Lean.mkConst (declName : Lean.Name) (us : optParam (List Lean.Level) []) :

mkConst declName us return .const declName us.

Equations

Lean.mkConst declName us = Lean.Expr.const declName us

def Lean.Literal.type :

Lean.Literal → Lean.Expr

Return the type of a literal value.

Equations

Lean.Literal.type x = match x with | Lean.Literal.natVal val => Lean.mkConst `Nat | Lean.Literal.strVal val => Lean.mkConst `String

@[export lean_lit_type]

def Lean.Literal.typeEx :

Lean.Literal → Lean.Expr

Equations

Lean.Literal.typeEx = Lean.Literal.type

def Lean.mkBVar (idx : Nat) :

.bvar idx is now the preferred form.

Equations

Lean.mkBVar idx = Lean.Expr.bvar idx

def Lean.mkSort (u : Lean.Level) :

.sort u is now the preferred form.

Equations

Lean.mkSort u = Lean.Expr.sort u

def Lean.mkFVar (fvarId : Lean.FVarId) :

.fvar fvarId is now the preferred form. This function is seldom used, free variables are often automatically created using the telescope functions (e.g., forallTelescope and lambdaTelescope) at MetaM.

Equations

Lean.mkFVar fvarId = Lean.Expr.fvar fvarId

def Lean.mkMVar (mvarId : Lean.MVarId) :

.mvar mvarId is now the preferred form. This function is seldom used, metavariables are often created using functions such as mkFresheExprMVar at MetaM.

Equations

Lean.mkMVar mvarId = Lean.Expr.mvar mvarId

def Lean.mkMData (m : Lean.MData) (e : Lean.Expr) :

.mdata m e is now the preferred form.

Equations

Lean.mkMData m e = Lean.Expr.mdata m e

def Lean.mkProj (structName : Lean.Name) (idx : Nat) (struct : Lean.Expr) :

.proj structName idx struct is now the preferred form.

Equations

Lean.mkProj structName idx struct = Lean.Expr.proj structName idx struct

def Lean.mkApp (f : Lean.Expr) (a : Lean.Expr) :

.app f a is now the preferred form.

Equations

Lean.mkApp f a = Lean.Expr.app f a

def Lean.mkLambda (x : Lean.Name) (bi : Lean.BinderInfo) (t : Lean.Expr) (b : Lean.Expr) :

.lam x t b bi is now the preferred form.

Equations

Lean.mkLambda x bi t b = Lean.Expr.lam x t b bi

def Lean.mkForall (x : Lean.Name) (bi : Lean.BinderInfo) (t : Lean.Expr) (b : Lean.Expr) :

.forallE x t b bi is now the preferred form.

Equations

Lean.mkForall x bi t b = Lean.Expr.forallE x t b bi

def Lean.mkSimpleThunkType (type : Lean.Expr) :

Return Unit -> type. Do not confuse with Thunk type

Equations

Lean.mkSimpleThunkType type = Lean.mkForall Lean.Name.anonymous Lean.BinderInfo.default (Lean.mkConst `Unit) type

def Lean.mkSimpleThunk (type : Lean.Expr) :

Return fun (_ : Unit), e

Equations

Lean.mkSimpleThunk type = Lean.mkLambda `_ Lean.BinderInfo.default (Lean.mkConst `Unit) type

def Lean.mkLet (x : Lean.Name) (t : Lean.Expr) (v : Lean.Expr) (b : Lean.Expr) (nonDep : optParam Bool false) :

.letE x t v b nonDep is now the preferred form.

Equations

Lean.mkLet x t v b nonDep = Lean.Expr.letE x t v b nonDep

def Lean.mkAppB (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) :

Equations

Lean.mkAppB f a b = Lean.mkApp (Lean.mkApp f a) b

def Lean.mkApp2 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) :

Equations

Lean.mkApp2 f a b = Lean.mkAppB f a b

def Lean.mkApp3 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) :

Equations

Lean.mkApp3 f a b c = Lean.mkApp (Lean.mkAppB f a b) c

def Lean.mkApp4 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) :

Equations

Lean.mkApp4 f a b c d = Lean.mkAppB (Lean.mkAppB f a b) c d

def Lean.mkApp5 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e : Lean.Expr) :

Equations

Lean.mkApp5 f a b c d e = Lean.mkApp (Lean.mkApp4 f a b c d) e

def Lean.mkApp6 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) :

Equations

Lean.mkApp6 f a b c d e₁ e₂ = Lean.mkAppB (Lean.mkApp4 f a b c d) e₁ e₂

def Lean.mkApp7 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) :

Equations

Lean.mkApp7 f a b c d e₁ e₂ e₃ = Lean.mkApp3 (Lean.mkApp4 f a b c d) e₁ e₂ e₃

def Lean.mkApp8 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) :

Equations

Lean.mkApp8 f a b c d e₁ e₂ e₃ e₄ = Lean.mkApp4 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄

def Lean.mkApp9 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) (e₅ : Lean.Expr) :

Equations

Lean.mkApp9 f a b c d e₁ e₂ e₃ e₄ e₅ = Lean.mkApp5 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅

def Lean.mkApp10 (f : Lean.Expr) (a : Lean.Expr) (b : Lean.Expr) (c : Lean.Expr) (d : Lean.Expr) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (e₃ : Lean.Expr) (e₄ : Lean.Expr) (e₅ : Lean.Expr) (e₆ : Lean.Expr) :

Equations

Lean.mkApp10 f a b c d e₁ e₂ e₃ e₄ e₅ e₆ = Lean.mkApp6 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆

def Lean.mkLit (l : Lean.Literal) :

.lit l is now the preferred form.

Equations

Lean.mkLit l = Lean.Expr.lit l

def Lean.mkRawNatLit (n : Nat) :

Return the "raw" natural number .lit (.natVal n). This is not the default representation used by the Lean frontend. See mkNatLit.

Equations

Lean.mkRawNatLit n = Lean.mkLit (Lean.Literal.natVal n)

def Lean.mkNatLit (n : Nat) :

Return a natural number literal used in the frontend. It is a OfNat.ofNat application. Recall that all theorems and definitions containing numeric literals are encoded using OfNat.ofNat applications in the frontend.

Equations

Lean.mkNatLit n = let r := Lean.mkRawNatLit n; Lean.mkApp3 (Lean.mkConst `OfNat.ofNat [Lean.levelZero]) (Lean.mkConst `Nat) r (Lean.mkApp (Lean.mkConst `instOfNatNat) r)

def Lean.mkStrLit (s : String) :

Return the string literal .lit (.strVal s)

Equations

Lean.mkStrLit s = Lean.mkLit (Lean.Literal.strVal s)

@[export lean_expr_mk_bvar]

def Lean.mkBVarEx :

Nat → Lean.Expr

Equations

Lean.mkBVarEx = Lean.mkBVar

@[export lean_expr_mk_fvar]

def Lean.mkFVarEx :

Lean.FVarId → Lean.Expr

Equations

Lean.mkFVarEx = Lean.mkFVar

@[export lean_expr_mk_mvar]

def Lean.mkMVarEx :

Lean.MVarId → Lean.Expr

Equations

Lean.mkMVarEx = Lean.mkMVar

@[export lean_expr_mk_sort]

def Lean.mkSortEx :

Lean.Level → Lean.Expr

Equations

Lean.mkSortEx = Lean.mkSort

@[export lean_expr_mk_const]

def Lean.mkConstEx (c : Lean.Name) (lvls : List Lean.Level) :

Equations

Lean.mkConstEx c lvls = Lean.mkConst c lvls

@[export lean_expr_mk_app]

def Lean.mkAppEx :

Lean.Expr → Lean.Expr → Lean.Expr

Equations

Lean.mkAppEx = Lean.mkApp

@[export lean_expr_mk_lambda]

def Lean.mkLambdaEx (n : Lean.Name) (d : Lean.Expr) (b : Lean.Expr) (bi : Lean.BinderInfo) :

Equations

Lean.mkLambdaEx n d b bi = Lean.mkLambda n bi d b

@[export lean_expr_mk_forall]

def Lean.mkForallEx (n : Lean.Name) (d : Lean.Expr) (b : Lean.Expr) (bi : Lean.BinderInfo) :

Equations

Lean.mkForallEx n d b bi = Lean.mkForall n bi d b

@[export lean_expr_mk_let]

def Lean.mkLetEx (n : Lean.Name) (t : Lean.Expr) (v : Lean.Expr) (b : Lean.Expr) :

Equations

Lean.mkLetEx n t v b = Lean.mkLet n t v b

@[export lean_expr_mk_lit]

def Lean.mkLitEx :

Lean.Literal → Lean.Expr

Equations

Lean.mkLitEx = Lean.mkLit

@[export lean_expr_mk_mdata]

def Lean.mkMDataEx :

Lean.MData → Lean.Expr → Lean.Expr

Equations

Lean.mkMDataEx = Lean.mkMData

@[export lean_expr_mk_proj]

def Lean.mkProjEx :

Lean.Name → Nat → Lean.Expr → Lean.Expr

Equations

Lean.mkProjEx = Lean.mkProj

def Lean.mkAppN (f : Lean.Expr) (args : Array Lean.Expr) :

mkAppN f #[a₀, ..., aₙ] ==> f a₀ a₁ .. aₙ

Equations

Lean.mkAppN f args = Array.foldl Lean.mkApp f args 0 (Array.size args)

def Lean.mkAppRange (f : Lean.Expr) (i : Nat) (j : Nat) (args : Array Lean.Expr) :

mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ] ==> the expression f a_i ... a_{j-1}

Equations

Lean.mkAppRange f i j args = Lean.mkAppRangeAux j args i f

def Lean.mkAppRev (fn : Lean.Expr) (revArgs : Array Lean.Expr) :

Same as mkApp f args but reversing args.

Equations

Lean.mkAppRev fn revArgs = Array.foldr (fun a r => Lean.mkApp r a) fn revArgs (Array.size revArgs)

@[extern lean_expr_dbg_to_string]

opaque Lean.Expr.dbgToString (e : Lean.Expr) :

String

@[extern lean_expr_quick_lt]

opaque Lean.Expr.quickLt (a : Lean.Expr) (b : Lean.Expr) :

A total order for expressions. We say it is quick because it first compares the hashcodes.

@[extern lean_expr_lt]

opaque Lean.Expr.lt (a : Lean.Expr) (b : Lean.Expr) :

A total order for expressions that takes the structure into account (e.g., variable names).

@[extern lean_expr_eqv]

opaque Lean.Expr.eqv (a : Lean.Expr) (b : Lean.Expr) :

Return true iff a and b are alpha equivalent. Binder annotations are ignored.

instance Lean.Expr.instBEqExpr :

BEq Lean.Expr

Equations

Lean.Expr.instBEqExpr = { beq := Lean.Expr.eqv }

@[extern lean_expr_equal]

opaque Lean.Expr.equal (a : Lean.Expr) (b : Lean.Expr) :

Return true iff a and b are equal. Binder names and annotations are taking into account.

def Lean.Expr.isSort :

Return true if the given expression is a .sort ..

Equations

Lean.Expr.isSort x = match x with | Lean.Expr.sort u => true | x => false

def Lean.Expr.isType :

Return true if the given expression is of the form .sort (.succ ..).

Equations

Lean.Expr.isType x = match x with | Lean.Expr.sort (Lean.Level.succ a) => true | x => false

def Lean.Expr.isType0 :

Return true if the given expression is of the form .sort (.succ .zero).

Equations

Lean.Expr.isType0 x = match x with | Lean.Expr.sort (Lean.Level.succ Lean.Level.zero) => true | x => false

def Lean.Expr.isProp :

Return true if the given expression is a .sort .zero

Equations

Lean.Expr.isProp x = match x with | Lean.Expr.sort Lean.Level.zero => true | x => false

def Lean.Expr.isBVar :

Return true if the given expression is a bound variable.

Equations

Lean.Expr.isBVar x = match x with | Lean.Expr.bvar deBruijnIndex => true | x => false

def Lean.Expr.isMVar :

Return true if the given expression is a metavariable.

Equations

Lean.Expr.isMVar x = match x with | Lean.Expr.mvar mvarId => true | x => false

def Lean.Expr.isFVar :

Return true if the given expression is a free variable.

Equations

Lean.Expr.isFVar x = match x with | Lean.Expr.fvar fvarId => true | x => false

def Lean.Expr.isApp :

Return true if the given expression is an application.

Equations

Lean.Expr.isApp x = match x with | Lean.Expr.app fn arg => true | x => false

def Lean.Expr.isProj :

Return true if the given expression is a projection .proj ..

Equations

Lean.Expr.isProj x = match x with | Lean.Expr.proj typeName idx struct => true | x => false

def Lean.Expr.isConst :

Return true if the given expression is a constant.

Equations

Lean.Expr.isConst x = match x with | Lean.Expr.const declName us => true | x => false

def Lean.Expr.isConstOf :

Lean.Expr → Lean.Name → Bool

Return true if the given expression is a constant of the give name. Examples:

(.const `Nat []).isConstOf `Nat is true
(.const `Nat []).isConstOf `False is false

Equations

Lean.Expr.isConstOf x x = match x, x with | Lean.Expr.const n us, m => n == m | x, x_1 => false

def Lean.Expr.isFVarOf :

Lean.Expr → Lean.FVarId → Bool

Return true if the given expression is a free variable with the given id. Examples:

isFVarOf (.fvar id) id is true
isFVarOf (.fvar id) id' is false
isFVarOf (.sort levelZero) id is false

Equations

Lean.Expr.isFVarOf x x = match x, x with | Lean.Expr.fvar fvarId, fvarId' => fvarId == fvarId' | x, x_1 => false

def Lean.Expr.isForall :

Return true if the given expression is a forall-expression aka (dependent) arrow.

Equations

Lean.Expr.isForall x = match x with | Lean.Expr.forallE binderName binderType body binderInfo => true | x => false

def Lean.Expr.isLambda :

Return true if the given expression is a lambda abstraction aka anonymous function.

Equations

Lean.Expr.isLambda x = match x with | Lean.Expr.lam binderName binderType body binderInfo => true | x => false

def Lean.Expr.isBinding :

Return true if the given expression is a forall or lambda expression.

Equations

Lean.Expr.isBinding x = match x with | Lean.Expr.lam binderName binderType body binderInfo => true | Lean.Expr.forallE binderName binderType body binderInfo => true | x => false

def Lean.Expr.isLet :

Return true if the given expression is a let-expression.

Equations

Lean.Expr.isLet x = match x with | Lean.Expr.letE declName type value body nonDep => true | x => false

def Lean.Expr.isMData :

Return true if the given expression is a metadata.

Equations

Lean.Expr.isMData x = match x with | Lean.Expr.mdata data expr => true | x => false

def Lean.Expr.isLit :

Return true if the given expression is a literal value.

Equations

Lean.Expr.isLit x = match x with | Lean.Expr.lit a => true | x => false

def Lean.Expr.getForallBody :

Return the "body" of a forall expression. Example: let e be the representation for forall (p : Prop) (q : Prop), p ∧ q, then getForallBody e returns .app (.app (.const `And []) (.bvar 1)) (.bvar 0)

Equations

Lean.Expr.getForallBody (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.Expr.getForallBody body
Lean.Expr.getForallBody x = x

def Lean.Expr.getForallBodyMaxDepth (maxDepth : Nat) :

Equations

Lean.Expr.getForallBodyMaxDepth (Nat.succ n) (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Expr.getForallBodyMaxDepth n b
Lean.Expr.getForallBodyMaxDepth 0 x = x
Lean.Expr.getForallBodyMaxDepth x x = x

def Lean.Expr.getForallBinderNames :

Lean.Expr → List Lean.Name

Given a sequence of nested foralls (a₁ : α₁) → ... → (aₙ : αₙ) → _, returns the names [a₁, ... aₙ].

Equations

Lean.Expr.getForallBinderNames (Lean.Expr.forallE binderName binderType body binderInfo) = binderName :: Lean.Expr.getForallBinderNames body
Lean.Expr.getForallBinderNames x = []

def Lean.Expr.getAppFn :

If the given expression is a sequence of function applications f a₁ .. aₙ, return f. Otherwise return the input expression.

Equations

Lean.Expr.getAppFn (Lean.Expr.app fn arg) = Lean.Expr.getAppFn fn
Lean.Expr.getAppFn x = x

def Lean.Expr.getAppNumArgs (e : Lean.Expr) :

Nat

Counts the number n of arguments for an expression f a₁ .. aₙ.

Equations

Lean.Expr.getAppNumArgs e = Lean.Expr.getAppNumArgsAux e 0

@[inline]

def Lean.Expr.getAppArgs (e : Lean.Expr) :

Array Lean.Expr

Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ]

Equations

Lean.Expr.getAppArgs e = let dummy := Lean.mkSort Lean.levelZero; let nargs := Lean.Expr.getAppNumArgs e; Lean.Expr.getAppArgsAux e (mkArray nargs dummy) (nargs - 1)

@[inline]

def Lean.Expr.getAppRevArgs (e : Lean.Expr) :

Array Lean.Expr

Same as getAppArgs but reverse the output array.

Equations

Lean.Expr.getAppRevArgs e = Lean.Expr.getAppRevArgsAux e (Array.mkEmpty (Lean.Expr.getAppNumArgs e))

@[specialize #[]]

def Lean.Expr.withAppAux {α : Sort u_1} (k : Lean.Expr → Array Lean.Expr → α) :

Lean.Expr → Array Lean.Expr → Nat → α

Equations

Lean.Expr.withAppAux k (Lean.Expr.app f a) x x = Lean.Expr.withAppAux k f (Array.set! x x a) (x - 1)
Lean.Expr.withAppAux k x x x = k x x

@[inline]

def Lean.Expr.withApp {α : Sort u_1} (e : Lean.Expr) (k : Lean.Expr → Array Lean.Expr → α) :

Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ].

Equations

Lean.Expr.withApp e k = let dummy := Lean.mkSort Lean.levelZero; let nargs := Lean.Expr.getAppNumArgs e; Lean.Expr.withAppAux k e (mkArray nargs dummy) (nargs - 1)

def Lean.Expr.traverseApp {M : Type → Type u_1} [inst : Monad M] (f : Lean.Expr → M Lean.Expr) (e : Lean.Expr) :

M Lean.Expr

Given e = fn a₁ ... aₙ, runs f on fn and each of the arguments aᵢ and makes a new function application with the results.

Equations

Lean.Expr.traverseApp f e = Lean.Expr.withApp e fun fn args => Seq.seq (Lean.mkAppN <$> f fn) fun x => Array.mapM f args

@[inline]

def Lean.Expr.withAppRev {α : Sort u_1} (e : Lean.Expr) (k : Lean.Expr → Array Lean.Expr → α) :

Same as withApp but with arguments reversed.

Equations

Lean.Expr.withAppRev e k = Lean.Expr.withAppRevAux k e (Array.mkEmpty (Lean.Expr.getAppNumArgs e))

def Lean.Expr.getRevArgD :

Lean.Expr → Nat → Lean.Expr → Lean.Expr

Equations

Lean.Expr.getRevArgD (Lean.Expr.app fn a) 0 x = a
Lean.Expr.getRevArgD (Lean.Expr.app f arg) (Nat.succ i) x = Lean.Expr.getRevArgD f i x
Lean.Expr.getRevArgD x x x = x

def Lean.Expr.getRevArg! :

Lean.Expr → Nat → Lean.Expr

Equations

Lean.Expr.getRevArg! (Lean.Expr.app fn a) 0 = a
Lean.Expr.getRevArg! (Lean.Expr.app f arg) (Nat.succ i) = Lean.Expr.getRevArg! f i
Lean.Expr.getRevArg! x x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 970 20 "invalid index"

@[inline]

def Lean.Expr.getArg! (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) :

Given f a₀ a₁ ... aₙ, returns the ith argument or panics if out of bounds.

Equations

Lean.Expr.getArg! e i n = Lean.Expr.getRevArg! e (n - i - 1)

@[inline]

def Lean.Expr.getArgD (e : Lean.Expr) (i : Nat) (v₀ : Lean.Expr) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) :

Given f a₀ a₁ ... aₙ, returns the ith argument or returns v₀ if out of bounds.

Equations

Lean.Expr.getArgD e i v₀ n = Lean.Expr.getRevArgD e (n - i - 1) v₀

def Lean.Expr.isAppOf (e : Lean.Expr) (n : Lean.Name) :

Given f a₀ a₁ ... aₙ, returns true if f is a constant with name n.

Equations

Lean.Expr.isAppOf e n = match Lean.Expr.getAppFn e with | Lean.Expr.const c us => c == n | x => false

def Lean.Expr.isAppOfArity :

Lean.Expr → Lean.Name → Nat → Bool

Given f a₁ ... aᵢ, returns true if f is a constant with name n and has the correct number of arguments.

Equations

Lean.Expr.isAppOfArity (Lean.Expr.const c us) x 0 = (c == x)
Lean.Expr.isAppOfArity (Lean.Expr.app f arg) x (Nat.succ a) = Lean.Expr.isAppOfArity f x a
Lean.Expr.isAppOfArity x x x = false

def Lean.Expr.isAppOfArity' :

Lean.Expr → Lean.Name → Nat → Bool

Similar to isAppOfArity but skips Expr.mdata.

Equations

Lean.Expr.isAppOfArity' (Lean.Expr.mdata data b) x x = Lean.Expr.isAppOfArity' b x x
Lean.Expr.isAppOfArity' (Lean.Expr.const c us) x 0 = (c == x)
Lean.Expr.isAppOfArity' (Lean.Expr.app f arg) x (Nat.succ a) = Lean.Expr.isAppOfArity' f x a
Lean.Expr.isAppOfArity' x x x = false

def Lean.Expr.appFn! :

Equations

Lean.Expr.appFn! x = match x with | Lean.Expr.app f arg => f | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!" 1004 15 "application expected"

def Lean.Expr.appArg! :

Equations

Lean.Expr.appArg! x = match x with | Lean.Expr.app fn a => a | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!" 1008 15 "application expected"

def Lean.Expr.appFn!' :

Equations

Lean.Expr.appFn!' (Lean.Expr.mdata data b) = Lean.Expr.appFn!' b
Lean.Expr.appFn!' (Lean.Expr.app f arg) = f
Lean.Expr.appFn!' x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!'" 1013 17 "application expected"

def Lean.Expr.appArg!' :

Equations

Lean.Expr.appArg!' (Lean.Expr.mdata data b) = Lean.Expr.appArg!' b
Lean.Expr.appArg!' (Lean.Expr.app f arg) = arg
Lean.Expr.appArg!' x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!'" 1018 17 "application expected"

def Lean.Expr.sortLevel! :

Lean.Expr → Lean.Level

Equations

Lean.Expr.sortLevel! x = match x with | Lean.Expr.sort u => u | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.sortLevel!" 1022 14 "sort expected"

def Lean.Expr.litValue! :

Lean.Expr → Lean.Literal

Equations

Lean.Expr.litValue! x = match x with | Lean.Expr.lit v => v | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.litValue!" 1026 13 "literal expected"

def Lean.Expr.isNatLit :

Equations

Lean.Expr.isNatLit x = match x with | Lean.Expr.lit (Lean.Literal.natVal val) => true | x => false

def Lean.Expr.natLit? :

Lean.Expr → Option Nat

Equations

Lean.Expr.natLit? x = match x with | Lean.Expr.lit (Lean.Literal.natVal v) => some v | x => none

def Lean.Expr.isStringLit :

Equations

Lean.Expr.isStringLit x = match x with | Lean.Expr.lit (Lean.Literal.strVal val) => true | x => false

def Lean.Expr.isCharLit (e : Lean.Expr) :

Equations

Lean.Expr.isCharLit e = (Lean.Expr.isAppOfArity e `Char.ofNat 1 && Lean.Expr.isNatLit (Lean.Expr.appArg! e))

def Lean.Expr.constName! :

Lean.Expr → Lean.Name

Equations

Lean.Expr.constName! x = match x with | Lean.Expr.const n us => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.constName!" 1045 17 "constant expected"

def Lean.Expr.constName? :

Lean.Expr → Option Lean.Name

Equations

Lean.Expr.constName? x = match x with | Lean.Expr.const n us => some n | x => none

def Lean.Expr.constLevels! :

Lean.Expr → List Lean.Level

Equations

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

def Lean.Expr.bvarIdx! :

Lean.Expr → Nat

Equations

Lean.Expr.bvarIdx! x = match x with | Lean.Expr.bvar idx => idx | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bvarIdx!" 1057 16 "bvar expected"

def Lean.Expr.fvarId! :

Lean.Expr → Lean.FVarId

Equations

Lean.Expr.fvarId! x = match x with | Lean.Expr.fvar n => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.fvarId!" 1061 14 "fvar expected"

def Lean.Expr.mvarId! :

Lean.Expr → Lean.MVarId

Equations

Lean.Expr.mvarId! x = match x with | Lean.Expr.mvar n => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mvarId!" 1065 14 "mvar expected"

def Lean.Expr.bindingName! :

Lean.Expr → Lean.Name

Equations

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

def Lean.Expr.bindingDomain! :

Equations

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

def Lean.Expr.bindingBody! :

Equations

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

def Lean.Expr.bindingInfo! :

Lean.Expr → Lean.BinderInfo

Equations

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

def Lean.Expr.letName! :

Lean.Expr → Lean.Name

Equations

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

def Lean.Expr.letType! :

Equations

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

def Lean.Expr.letValue! :

Equations

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

def Lean.Expr.letBody! :

Equations

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

def Lean.Expr.consumeMData :

Equations

Lean.Expr.consumeMData (Lean.Expr.mdata data expr) = Lean.Expr.consumeMData expr
Lean.Expr.consumeMData x = x

def Lean.Expr.mdataExpr! :

Equations

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

def Lean.Expr.projExpr! :

Equations

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

def Lean.Expr.projIdx! :

Lean.Expr → Nat

Equations

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

def Lean.Expr.hasLooseBVars (e : Lean.Expr) :

Equations

Lean.Expr.hasLooseBVars e = decide (Lean.Expr.looseBVarRange e > 0)

def Lean.Expr.isArrow (e : Lean.Expr) :

Return true if e is a non-dependent arrow. Remark: the following function assumes e does not have loose bound variables.

Equations

Lean.Expr.isArrow e = match e with | Lean.Expr.forallE binderName binderType b binderInfo => !Lean.Expr.hasLooseBVars b | x => false

@[extern lean_expr_has_loose_bvar]

opaque Lean.Expr.hasLooseBVar (e : Lean.Expr) (bvarIdx : Nat) :

def Lean.Expr.hasLooseBVarInExplicitDomain :

Lean.Expr → Nat → Bool → Bool

Return true if e contains the loose bound variable bvarIdx in an explicit parameter, or in the range if tryRange == true.

Equations

One or more equations did not get rendered due to their size.
Lean.Expr.hasLooseBVarInExplicitDomain x x x = (x && Lean.Expr.hasLooseBVar x x)

@[extern lean_expr_lower_loose_bvars]

opaque Lean.Expr.lowerLooseBVars (e : Lean.Expr) (s : Nat) (d : Nat) :

Lower the loose bound variables >= s in e by d. That is, a loose bound variable bvar i. i >= s is mapped into bvar (i-d).

Remark: if s < d, then result is e

@[extern lean_expr_lift_loose_bvars]

opaque Lean.Expr.liftLooseBVars (e : Lean.Expr) (s : Nat) (d : Nat) :

Lift loose bound variables >= s in e by d.

def Lean.Expr.inferImplicit :

Lean.Expr → Nat → Bool → Lean.Expr

inferImplicit e numParams considerRange updates the first numParams parameter binder annotations of the e forall type. It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or the resulting type if considerRange == true.

Remark: we use this function to infer the bind annotations of inductive datatype constructors, and structure projections. When the {} annotation is used in these commands, we set considerRange == false.

@[extern lean_expr_instantiate]

opaque Lean.Expr.instantiate (e : Lean.Expr) (subst : Array Lean.Expr) :

Instantiate the loose bound variables in e using subst. That is, a loose Expr.bvar i is replaced with subst[i].

@[extern lean_expr_instantiate1]

opaque Lean.Expr.instantiate1 (e : Lean.Expr) (subst : Lean.Expr) :

@[extern lean_expr_instantiate_rev]

opaque Lean.Expr.instantiateRev (e : Lean.Expr) (subst : Array Lean.Expr) :

Similar to instantiate, but Expr.bvar i is replaced with subst[subst.size - i - 1]

@[extern lean_expr_instantiate_range]

opaque Lean.Expr.instantiateRange (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (xs : Array Lean.Expr) :

Similar to instantiate, but consider only the variables xs in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= xs.size does not hold.

@[extern lean_expr_instantiate_rev_range]

opaque Lean.Expr.instantiateRevRange (e : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (xs : Array Lean.Expr) :

Similar to instantiateRev, but consider only the variables xs in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= xs.size does not hold.

@[extern lean_expr_abstract]

opaque Lean.Expr.abstract (e : Lean.Expr) (xs : Array Lean.Expr) :

Replace free (or meta) variables xs with loose bound variables.

@[extern lean_expr_abstract_range]

opaque Lean.Expr.abstractRange (e : Lean.Expr) (n : Nat) (xs : Array Lean.Expr) :

Similar to abstract, but consider only the first min n xs.size entries in xs.

def Lean.Expr.replaceFVar (e : Lean.Expr) (fvar : Lean.Expr) (v : Lean.Expr) :

Replace occurrences of the free variable fvar in e with v

Equations

Lean.Expr.replaceFVar e fvar v = Lean.Expr.instantiate1 (Lean.Expr.abstract e #[fvar]) v

def Lean.Expr.replaceFVarId (e : Lean.Expr) (fvarId : Lean.FVarId) (v : Lean.Expr) :

Replace occurrences of the free variable fvarId in e with v

Equations

Lean.Expr.replaceFVarId e fvarId v = Lean.Expr.replaceFVar e (Lean.mkFVar fvarId) v

def Lean.Expr.replaceFVars (e : Lean.Expr) (fvars : Array Lean.Expr) (vs : Array Lean.Expr) :

Replace occurrences of the free variables fvars in e with vs

Equations

Lean.Expr.replaceFVars e fvars vs = Lean.Expr.instantiateRev (Lean.Expr.abstract e fvars) vs

instance Lean.Expr.instToStringExpr :

ToString Lean.Expr

Equations

Lean.Expr.instToStringExpr = { toString := Lean.Expr.dbgToString }

def Lean.Expr.isAtomic :

Returns true when the expression does not have any sub-expressions.

Equations

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

def Lean.mkDecIsTrue (pred : Lean.Expr) (proof : Lean.Expr) :

Equations

Lean.mkDecIsTrue pred proof = Lean.mkAppB (Lean.mkConst `Decidable.isTrue) pred proof

def Lean.mkDecIsFalse (pred : Lean.Expr) (proof : Lean.Expr) :

Equations

Lean.mkDecIsFalse pred proof = Lean.mkAppB (Lean.mkConst `Decidable.isFalse) pred proof

@[inline]

abbrev Lean.ExprMap (α : Type) :

Equations

Lean.ExprMap α = Lean.HashMap Lean.Expr α

@[inline]

abbrev Lean.PersistentExprMap (α : Type) :

Equations

Lean.PersistentExprMap α = Lean.PHashMap Lean.Expr α

@[inline]

abbrev Lean.ExprSet :

Equations

Lean.ExprSet = Lean.HashSet Lean.Expr

@[inline]

abbrev Lean.PersistentExprSet :

Equations

Lean.PersistentExprSet = Lean.PHashSet Lean.Expr

@[inline]

abbrev Lean.PExprSet :

Equations

Lean.PExprSet = Lean.PersistentExprSet

structure Lean.ExprStructEq :

val : Lean.Expr

Auxiliary type for forcing == to be structural equality for Expr

Instances For

Inhabited Lean.ExprStructEq

instance Lean.instInhabitedExprStructEq :

Equations

Lean.instInhabitedExprStructEq = { default := { val := default } }

Coe Lean.Expr Lean.ExprStructEq

instance Lean.instCoeExprExprStructEq :

Equations

Lean.instCoeExprExprStructEq = { coe := Lean.ExprStructEq.mk }

def Lean.ExprStructEq.beq :

Lean.ExprStructEq → Lean.ExprStructEq → Bool

Equations

Lean.ExprStructEq.beq x x = match x, x with | { val := e₁ }, { val := e₂ } => Lean.Expr.equal e₁ e₂

def Lean.ExprStructEq.hash :

Lean.ExprStructEq → UInt64

Equations

Lean.ExprStructEq.hash x = match x with | { val := e } => Lean.Expr.hash e

instance Lean.ExprStructEq.instBEqExprStructEq :

BEq Lean.ExprStructEq

Equations

Lean.ExprStructEq.instBEqExprStructEq = { beq := Lean.ExprStructEq.beq }

Hashable Lean.ExprStructEq

instance Lean.ExprStructEq.instHashableExprStructEq :

Equations

Lean.ExprStructEq.instHashableExprStructEq = { hash := Lean.ExprStructEq.hash }

ToString Lean.ExprStructEq

instance Lean.ExprStructEq.instToStringExprStructEq :

Equations

Lean.ExprStructEq.instToStringExprStructEq = { toString := fun e => toString e.val }

@[inline]

abbrev Lean.ExprStructMap (α : Type) :

Equations

Lean.ExprStructMap α = Lean.HashMap Lean.ExprStructEq α

@[inline]

abbrev Lean.PersistentExprStructMap (α : Type) :

Equations

Lean.PersistentExprStructMap α = Lean.PHashMap Lean.ExprStructEq α

def Lean.Expr.mkAppRevRange (f : Lean.Expr) (beginIdx : Nat) (endIdx : Nat) (revArgs : Array Lean.Expr) :

mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)

Equations

Lean.Expr.mkAppRevRange f beginIdx endIdx revArgs = Lean.Expr.mkAppRevRangeAux revArgs beginIdx f endIdx

def Lean.Expr.betaRev (f : Lean.Expr) (revArgs : Array Lean.Expr) (useZeta : optParam Bool false) (preserveMData : optParam Bool false) :

If f is a lambda expression, than "beta-reduce" it using revArgs. This function is often used with getAppRev or withAppRev. Examples:

betaRev (fun x y => t x y) #[] ==> fun x y => t x y
betaRev (fun x y => t x y) #[a] ==> fun y => t a y
betaRev (fun x y => t x y) #[a, b] ==> t b a
betaRev (fun x y => t x y) #[a, b, c, d] ==> t d c b a Suppose t is (fun x y => t x y) a b c d, then args := t.getAppRev is #[d, c, b, a], and betaRev (fun x y => t x y) #[d, c, b, a] is t a b c d.

If useZeta is true, the function also performs zeta-reduction (reduction of let binders) to create further opportunities for beta reduction.

Equations

Lean.Expr.betaRev f revArgs useZeta preserveMData = if (Array.size revArgs == 0) = true then f else let sz := Array.size revArgs; Lean.Expr.betaRev.go revArgs useZeta preserveMData sz f 0

partial def Lean.Expr.betaRev.go (revArgs : Array Lean.Expr) (useZeta : optParam Bool false) (preserveMData : optParam Bool false) (sz : Nat) (e : Lean.Expr) (i : Nat) :

def Lean.Expr.beta (f : Lean.Expr) (args : Array Lean.Expr) :

Apply the given arguments to f, beta-reducing if f is a lambda expression. See docstring for betaRev for examples.

Equations

Lean.Expr.beta f args = Lean.Expr.betaRev f (Array.reverse args) false

def Lean.Expr.isHeadBetaTargetFn (useZeta : Bool) :

Return true if the given expression is the function of an expression that is target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

See isHeadBetaTarget.

Equations

Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.lam binderName binderType b binderInfo) = true
Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.letE declName type v b nonDep) = (useZeta && Lean.Expr.isHeadBetaTargetFn useZeta b)
Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.mdata k b) = Lean.Expr.isHeadBetaTargetFn useZeta b
Lean.Expr.isHeadBetaTargetFn useZeta x = false

def Lean.Expr.headBeta (e : Lean.Expr) :

(fun x => e) a ==> e[x/a].

Equations

Lean.Expr.headBeta e = let f := Lean.Expr.getAppFn e; if Lean.Expr.isHeadBetaTargetFn false f = true then Lean.Expr.betaRev f (Lean.Expr.getAppRevArgs e) false else e

def Lean.Expr.isHeadBetaTarget (e : Lean.Expr) (useZeta : optParam Bool false) :

Return true if the given expression is a target for (head) beta reduction. If useZeta = true, then let-expressions are visited. That is, it assumes that zeta-reduction (aka let-expansion) is going to be used.

Equations

Lean.Expr.isHeadBetaTarget e useZeta = (Lean.Expr.isApp e && Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.getAppFn e))

def Lean.Expr.etaExpanded? (e : Lean.Expr) :

If e is of the form (fun x₁ ... xₙ => f x₁ ... xₙ) and f does not contain x₁, ..., xₙ, then return some f. Otherwise, return none.

It assumes e does not have loose bound variables.

Remark: ₙ may be 0

Equations

Lean.Expr.etaExpanded? e = Lean.Expr.etaExpandedAux e 0

def Lean.Expr.etaExpandedStrict? :

Lean.Expr → Option Lean.Expr

Similar to etaExpanded?, but only succeeds if ₙ ≥ 1.

Equations

Lean.Expr.etaExpandedStrict? x = match x with | Lean.Expr.lam binderName binderType b binderInfo => Lean.Expr.etaExpandedAux b 1 | x => none

def Lean.Expr.getOptParamDefault? (e : Lean.Expr) :

Return some e' if e is of the form optParam _ e'

Equations

Lean.Expr.getOptParamDefault? e = if Lean.Expr.isAppOfArity e `optParam 2 = true then some (Lean.Expr.appArg! e) else none

def Lean.Expr.getAutoParamTactic? (e : Lean.Expr) :

Return some e' if e is of the form autoParam _ e'

Equations

Lean.Expr.getAutoParamTactic? e = if Lean.Expr.isAppOfArity e `autoParam 2 = true then some (Lean.Expr.appArg! e) else none

@[export lean_is_out_param]

def Lean.Expr.isOutParam (e : Lean.Expr) :

Return true if e is of the form outParam _

Equations

Lean.Expr.isOutParam e = Lean.Expr.isAppOfArity e `outParam 1

def Lean.Expr.isOptParam (e : Lean.Expr) :

Return true if e is of the form optParam _ _

Equations

Lean.Expr.isOptParam e = Lean.Expr.isAppOfArity e `optParam 2

def Lean.Expr.isAutoParam (e : Lean.Expr) :

Return true if e is of the form autoParam _ _

Equations

Lean.Expr.isAutoParam e = Lean.Expr.isAppOfArity e `autoParam 2

@[export lean_expr_consume_type_annotations]

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

Remove outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

Given e of the form outParam (optParam Nat b), consumeTypeAnnotations e = b.
Given e of the form Nat → outParam (optParam Nat b), consumeTypeAnnotations e = e.

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

Remove metadata annotations and outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

Given e of the form outParam (optParam Nat b), cleanupAnnotations e = b.
Given e of the form Nat → outParam (optParam Nat b), cleanupAnnotations e = e.

@[inline]

def Lean.Expr.hasAnyFVar (e : Lean.Expr) (p : Lean.FVarId → Bool) :

Return true iff e contains a free variable which statisfies p.

Equations

Lean.Expr.hasAnyFVar e p = Lean.Expr.hasAnyFVar.visit p e

@[specialize #[]]

def Lean.Expr.hasAnyFVar.visit (p : Lean.FVarId → Bool) (e : Lean.Expr) :

def Lean.Expr.containsFVar (e : Lean.Expr) (fvarId : Lean.FVarId) :

Return true if e contains the given free variable.

Equations

Lean.Expr.containsFVar e fvarId = Lean.Expr.hasAnyFVar e fun x => x == fvarId

The update functions try to avoid allocating new values using pointer equality. Note that if the update*! functions are used under a match-expression, the compiler will eliminate the double-match.

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateApp!Impl]

def Lean.Expr.updateApp! (e : Lean.Expr) (newFn : Lean.Expr) (newArg : Lean.Expr) :

Equations

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

@[inline]

def Lean.Expr.updateFVar! (e : Lean.Expr) (fvarIdNew : Lean.FVarId) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateConst!Impl]

def Lean.Expr.updateConst! (e : Lean.Expr) (newLevels : List Lean.Level) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateSort!Impl]

def Lean.Expr.updateSort! (e : Lean.Expr) (newLevel : Lean.Level) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateMData!Impl]

def Lean.Expr.updateMData! (e : Lean.Expr) (newExpr : Lean.Expr) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateProj!Impl]

def Lean.Expr.updateProj! (e : Lean.Expr) (newExpr : Lean.Expr) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateForall!Impl]

def Lean.Expr.updateForall! (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) :

Equations

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

@[inline]

def Lean.Expr.updateForallE! (e : Lean.Expr) (newDomain : Lean.Expr) (newBody : Lean.Expr) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLambda!Impl]

def Lean.Expr.updateLambda! (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) :

Equations

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

@[inline]

def Lean.Expr.updateLambdaE! (e : Lean.Expr) (newDomain : Lean.Expr) (newBody : Lean.Expr) :

Equations

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

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLet!Impl]

def Lean.Expr.updateLet! (e : Lean.Expr) (newType : Lean.Expr) (newVal : Lean.Expr) (newBody : Lean.Expr) :

Equations

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

def Lean.Expr.updateFn :

Lean.Expr → Lean.Expr → Lean.Expr

Equations

Lean.Expr.updateFn (Lean.Expr.app f a) x = Lean.Expr.updateApp! (Lean.Expr.app f a) (Lean.Expr.updateFn f x) a
Lean.Expr.updateFn x x = x

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

Eta reduction. If e is of the form (fun x => f x), then return f.

def Lean.Expr.setOption {α : Type} (e : Lean.Expr) (optionName : Lean.Name) [inst : Lean.KVMap.Value α] (val : α) :

Annotate e with the given option. The information is stored using metadata around e.

Equations

Lean.Expr.setOption e optionName val = Lean.mkMData (Lean.KVMap.set Lean.MData.empty optionName val) e

def Lean.Expr.setPPExplicit (e : Lean.Expr) (flag : Bool) :

Annotate e with pp.explicit := flag The delaborator uses pp options.

Equations

Lean.Expr.setPPExplicit e flag = Lean.Expr.setOption e `pp.explicit flag

def Lean.Expr.setPPUniverses (e : Lean.Expr) (flag : Bool) :

Annotate e with pp.universes := flag The delaborator uses pp options.

Equations

Lean.Expr.setPPUniverses e flag = Lean.Expr.setOption e `pp.universes flag

def Lean.Expr.setAppPPExplicit (e : Lean.Expr) :

If e is an application f a_1 ... a_n annotate f, a_1 ... a_n with pp.explicit := false, and annotate e with pp.explicit := true.

Equations

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

def Lean.Expr.setAppPPExplicitForExposingMVars (e : Lean.Expr) :

Similar for setAppPPExplicit, but only annotate children with pp.explicit := false if e does not contain metavariables.

Equations

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

def Lean.mkAnnotation (kind : Lean.Name) (e : Lean.Expr) :

Annotate e with the given annotation name kind. It uses metadata to store the annotation.

Equations

Lean.mkAnnotation kind e = Lean.mkMData (Lean.KVMap.insert Lean.KVMap.empty kind (Lean.DataValue.ofBool true)) e

def Lean.annotation? (kind : Lean.Name) (e : Lean.Expr) :

Return some e' if e = mkAnnotation kind e'

Equations

Lean.annotation? kind e = match e with | Lean.Expr.mdata d b => if (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d kind) = true then some b else none | x => none

def Lean.mkLetFunAnnotation (e : Lean.Expr) :

Annotate e with the let_fun annotation. This annotation is used as hint for the delaborator. If e is of the form (fun x : t => b) v, then mkLetFunAnnotation e is delaborated at let_fun x : t := v; b

Equations

Lean.mkLetFunAnnotation e = Lean.mkAnnotation `let_fun e

def Lean.letFunAnnotation? (e : Lean.Expr) :

Return some e' if e = mkLetFunAnnotation e'

Equations

Lean.letFunAnnotation? e = Lean.annotation? `let_fun e

def Lean.isLetFun (e : Lean.Expr) :

Return true if e = mkLetFunAnnotation e', and e' is of the form (fun x : t => b) v

Equations

Lean.isLetFun e = match Lean.letFunAnnotation? e with | none => false | some e => Lean.Expr.isApp e && Lean.Expr.isLambda (Lean.Expr.appFn! e)

def Lean.mkInaccessible (e : Lean.Expr) :

Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t) and _ in patterns.

Equations

Lean.mkInaccessible e = Lean.mkAnnotation `_inaccessible e

def Lean.inaccessible? (e : Lean.Expr) :

Return some e' if e = mkInaccessible e'.

Equations

Lean.inaccessible? e = Lean.annotation? `_inaccessible e

def Lean.patternWithRef? (p : Lean.Expr) :

Option (Lean.Syntax × Lean.Expr)

During elaboration expressions corresponding to pattern matching terms are annotated with Syntax objects. This function returns some (stx, p') if p is the pattern p' annotated with stx

Equations

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

def Lean.isPatternWithRef (p : Lean.Expr) :

Equations

Lean.isPatternWithRef p = Option.isSome (Lean.patternWithRef? p)

def Lean.mkPatternWithRef (p : Lean.Expr) (stx : Lean.Syntax) :

Annotate the pattern p with stx. This is an auxiliary annotation for producing better hover information.

Equations

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

def Lean.patternAnnotation? (e : Lean.Expr) :

Return some p if e is an annotated pattern (inaccessible? or patternWithRef?)

Equations

Lean.patternAnnotation? e = match Lean.inaccessible? e with | some e => some e | x => match Lean.patternWithRef? e with | some (fst, e) => some e | x => none

def Lean.mkLHSGoalRaw (e : Lean.Expr) :

Annotate e with the LHS annotation. The delaborator displays expressions of the form lhs = rhs as lhs when they have this annotation. This is used to implement the infoview for the conv mode.

This version of mkLHSGoal does not check that the argument is an equality.

Equations

Lean.mkLHSGoalRaw e = Lean.mkAnnotation `_lhsGoal e

def Lean.isLHSGoal? (e : Lean.Expr) :

Return some lhs if e = mkLHSGoal e', where e' is of the form lhs = rhs.

Equations

Lean.isLHSGoal? e = match Lean.annotation? `_lhsGoal e with | none => none | some e => if Lean.Expr.isAppOfArity e `Eq 3 = true then some (Lean.Expr.appArg! (Lean.Expr.appFn! e)) else none

def Lean.mkFreshFVarId {m : Type → Type} [inst : Monad m] [inst : Lean.MonadNameGenerator m] :

m Lean.FVarId

Polymorphic operation for generating unique/fresh free variable identifiers. It is available in any monad m that implements the inferface MonadNameGenerator.

Equations

Lean.mkFreshFVarId = do let __do_lift ← Lean.mkFreshId pure { name := __do_lift }

def Lean.mkFreshMVarId {m : Type → Type} [inst : Monad m] [inst : Lean.MonadNameGenerator m] :

m Lean.MVarId

Polymorphic operation for generating unique/fresh metavariable identifiers. It is available in any monad m that implements the inferface MonadNameGenerator.

Equations

Lean.mkFreshMVarId = do let __do_lift ← Lean.mkFreshId pure { name := __do_lift }