Lean.Meta.ExprDefEq

source

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

Lean.MetaM Lean.LBool

Equations

Lean.Meta.isDefEqNative s t = let isDefEq := fun s t => toLBoolM (Lean.Meta.isExprDefEqAux s t); do let s? ← Lean.Meta.reduceNative? s let t? ← Lean.Meta.reduceNative? t match s?, t? with | some s, some t => isDefEq s t | some s, none => isDefEq s t | none, some t => isDefEq s t | none, none => pure Lean.LBool.undef

source

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

Lean.MetaM Lean.LBool

Equations

Lean.Meta.isDefEqNat s t = let isDefEq := fun s t => toLBoolM (Lean.Meta.isExprDefEqAux s t); if (Lean.Expr.hasFVar s || Lean.Expr.hasMVar s || Lean.Expr.hasFVar t || Lean.Expr.hasMVar t) = true then pure Lean.LBool.undef else do let s? ← Lean.Meta.reduceNat? s let t? ← Lean.Meta.reduceNat? t match s?, t? with | some s, some t => isDefEq s t | some s, none => isDefEq s t | none, some t => isDefEq s t | none, none => pure Lean.LBool.undef

source

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

Lean.MetaM Lean.LBool

Equations

Lean.Meta.isDefEqStringLit s t = let isDefEq := fun s t => toLBoolM (Lean.Meta.isExprDefEqAux s t); if (Lean.Expr.isStringLit s && Lean.Expr.isAppOf t `String.mk) = true then isDefEq (Lean.Meta.toCtorIfLit s) t else if (Lean.Expr.isAppOf s `String.mk && Lean.Expr.isStringLit t) = true then isDefEq s (Lean.Meta.toCtorIfLit t) else pure Lean.LBool.undef

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isEtaUnassignedMVar e = match Lean.Expr.etaExpanded? e with | some (Lean.Expr.mvar mvarId x) => do let a ← Lean.Meta.isReadOnlyOrSyntheticOpaqueExprMVar mvarId if a = true then pure false else do let a ← Lean.Meta.isExprMVarAssigned mvarId if a = true then pure false else pure true | x => pure false

source

@[specialize]

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

Lean.MetaM Bool

Equations

Lean.Meta.isDefEqBindingDomain fvars ds₂ k = (fun loop => loop 0) (Lean.Meta.isDefEqBindingDomain.loop fvars ds₂ k)

source

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

Lean.MetaM Bool

source

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

source

constant Lean.Meta.CheckAssignment.checkAssignmentExceptionId :

Lean.InternalExceptionId

source

constant Lean.Meta.CheckAssignment.outOfScopeExceptionId :

Lean.InternalExceptionId

source

structure Lean.Meta.CheckAssignment.State :

Type

cache : Lean.ExprStructMap Lean.Expr

source

structure Lean.Meta.CheckAssignment.Context :

Type

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

source

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

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

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

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM α

Equations

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

source

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 }

source

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

Lean.Meta.CheckAssignment.run x mvarId fvars hasCtxLocals v = do let mvarDecl ← Lean.Meta.getMVarDecl mvarId let ctx : Lean.Meta.CheckAssignment.Context := { mvarId := mvarId, mvarDecl := mvarDecl, fvars := fvars, hasCtxLocals := hasCtxLocals, rhs := v } let x : Lean.Meta.CheckAssignment.CheckAssignmentM (Option Lean.Expr) := Lean.catchInternalIds [Lean.Meta.CheckAssignment.outOfScopeExceptionId, Lean.Meta.CheckAssignment.checkAssignmentExceptionId] (do let e ← x pure (some e)) fun x => pure none StateRefT'.run' (ReaderT.run x ctx) { cache := ∅ }

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

source

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

Lean.MetaM Bool

source

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

Lean.MetaM (Option Lean.Expr)

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

source

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

Lean.Meta.CheckAssignment.CheckAssignmentM Lean.Expr

source

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

Bool

Equations

Lean.Meta.CheckAssignmentQuick.check hasCtxLocals ctxApprox mctx lctx mvarDecl mvarId fvars e = (fun visit => visit e) (Lean.Meta.CheckAssignmentQuick.check.visit hasCtxLocals mctx lctx mvarDecl mvarId fvars)

source

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

Bool

source

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

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.checkAssignment mvarId fvars v = do let r ← forIn fvars { fst := none, snd := PUnit.unit } fun fvar r => let r := r.snd; do let a ← Lean.Meta.inferType fvar let a ← Lean.Meta.occursCheck mvarId a if a = true then do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) else pure (ForInStep.done { fst := some none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (Option Lean.Expr) := fun y => if (!Lean.Expr.hasExprMVar v && !Lean.Expr.hasFVar v) = true then pure (some v) else do let mvarDecl ← Lean.Meta.getMVarDecl mvarId let hasCtxLocals : Bool := Array.any fvars (fun fvar => Lean.LocalContext.containsFVar mvarDecl.lctx fvar) 0 (Array.size fvars) let ctx ← read let mctx ← Lean.getMCtx if Lean.Meta.CheckAssignmentQuick.check hasCtxLocals ctx.config.ctxApprox mctx ctx.lctx mvarDecl mvarId fvars v = true then pure (some v) else do let v ← Lean.Meta.instantiateMVars v Lean.Meta.CheckAssignment.checkAssignmentAux mvarId fvars hasCtxLocals v match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

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

source

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

Lean.MetaM Bool