Documentation

Lean.Meta.ExprDefEq

def Lean.Meta.isDefEqNative (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for Lean.reduceBool and Lean.reduceNat

Equations

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

def Lean.Meta.isDefEqNat (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for reducing Nat basic operations.

Equations

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

def Lean.Meta.isDefEqStringLit (s : Lean.Expr) (t : Lean.Expr) :

Lean.MetaM Lean.LBool

Support for constraints of the form ("..." =?= String.mk cs)

Equations

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

def Lean.Meta.isEtaUnassignedMVar (e : Lean.Expr) :

Lean.MetaM Bool

Return true if e is of the form fun (x_1 ... x_n) => ?m x_1 ... x_n), and ?m is unassigned. Remark: n may be 0.

Equations

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

@[specialize]

def Lean.Meta.isDefEqBindingDomain (fvars : Array Lean.Expr) (ds₂ : Array Lean.Expr) (k : Lean.MetaM Bool) :

Lean.MetaM Bool

Check whether the types of the free variables at fvars are definitionally equal to the types at ds₂.

Pre: fvars.size == ds₂.size

This method also updates the set of local instances, and invokes the continuation k with the updated set.

We can't use withNewLocalInstances because the isDeq fvarType d₂ may use local instances.

Equations

Lean.Meta.isDefEqBindingDomain fvars ds₂ k = Lean.Meta.isDefEqBindingDomain.loop fvars ds₂ k 0

partial def Lean.Meta.isDefEqBindingDomain.loop (fvars : Array Lean.Expr) (ds₂ : Array Lean.Expr) (k : Lean.MetaM Bool) (i : Nat) :

Lean.MetaM Bool

def Lean.Meta.mkAuxMVar (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (type : Lean.Expr) (numScopeArgs : optParam Nat 0) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAuxMVar lctx localInsts type numScopeArgs = Lean.Meta.mkFreshExprMVarAt lctx localInsts type Lean.MetavarKind.natural Lean.Name.anonymous numScopeArgs

opaque Lean.Meta.CheckAssignment.checkAssignmentExceptionId:

Lean.InternalExceptionId

opaque Lean.Meta.CheckAssignment.outOfScopeExceptionId:

Lean.InternalExceptionId

structure Lean.Meta.CheckAssignment.State:

Type

cache : Lean.ExprStructMap Lean.Expr

structure Lean.Meta.CheckAssignment.Context:

Type

mvarId : Lean.MVarId
mvarDecl : Lean.MetavarDecl
fvars : Array Lean.Expr
hasCtxLocals : Bool
rhs : Lean.Expr

@[inline]

abbrev Lean.Meta.CheckAssignment.CheckAssignmentM (α : Type) :

Type

Equations

Lean.Meta.CheckAssignment.CheckAssignmentM = ReaderT Lean.Meta.CheckAssignment.Context (StateRefT' IO.RealWorld Lean.Meta.CheckAssignment.State Lean.MetaM)

def Lean.Meta.CheckAssignment.throwCheckAssignmentFailure {α : Type} :

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

Lean.Meta.CheckAssignment.throwCheckAssignmentFailure = throw (Lean.Exception.internal Lean.Meta.CheckAssignment.checkAssignmentExceptionId)

def Lean.Meta.CheckAssignment.throwOutOfScopeFVar {α : Type} :

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

Lean.Meta.CheckAssignment.throwOutOfScopeFVar = throw (Lean.Exception.internal Lean.Meta.CheckAssignment.outOfScopeExceptionId)

instance Lean.Meta.CheckAssignment.instMonadCacheExprCheckAssignmentM:

Lean.MonadCache Lean.Expr Lean.Expr Lean.Meta.CheckAssignment.CheckAssignmentM

Equations

Lean.Meta.CheckAssignment.instMonadCacheExprCheckAssignmentM = { findCached? := Lean.Meta.CheckAssignment.findCached?, cache := Lean.Meta.CheckAssignment.cache }

@[inline]

def Lean.Meta.CheckAssignment.run (x : Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (hasCtxLocals : Bool) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

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

partial def Lean.Meta.CheckAssignment.checkFVar (fvar : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.checkMVar (mvar : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.assignToConstFun (mvar : Lean.Expr) (numArgs : Nat) (newMVar : Lean.Expr) :

Lean.MetaM Bool

partial def Lean.Meta.CheckAssignment.checkAssignmentAux (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (hasCtxLocals : Bool) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

partial def Lean.Meta.CheckAssignment.checkApp (e : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

partial def Lean.Meta.CheckAssignment.check (e : Lean.Expr) :

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

def Lean.Meta.CheckAssignmentQuick.check (hasCtxLocals : Bool) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (mvarDecl : Lean.MetavarDecl) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (e : Lean.Expr) :

Equations

Lean.Meta.CheckAssignmentQuick.check hasCtxLocals mctx lctx mvarDecl mvarId fvars e = Lean.Meta.CheckAssignmentQuick.check.visit hasCtxLocals mctx lctx mvarDecl mvarId fvars e

partial def Lean.Meta.CheckAssignmentQuick.check.visit (hasCtxLocals : Bool) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (mvarDecl : Lean.MetavarDecl) (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (e : Lean.Expr) :

def Lean.Meta.checkAssignment (mvarId : Lean.MVarId) (fvars : Array Lean.Expr) (v : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Auxiliary function for handling constraints of the form ?m a₁ ... aₙ =?= v. It will check whether we can perform the assignment

?m := fun fvars => v

The result is none if the assignment can't be performed. The result is some newV where newV is a possibly updated v. This method may need to unfold let-declarations.

Equations

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

@[inline]

def Lean.Meta.whenUndefDo (x : Lean.MetaM Lean.LBool) (k : Lean.MetaM Bool) :

Lean.MetaM Bool

Equations

Lean.Meta.whenUndefDo x k = do let status ← x match status with | Lean.LBool.true => pure true | Lean.LBool.false => pure false | Lean.LBool.undef => k

@[export lean_is_expr_def_eq]

partial def Lean.Meta.isExprDefEqAuxImpl (t : Lean.Expr) (s : Lean.Expr) :

Lean.MetaM Bool