Auxiliary function for instantiating the loose bound variables in e with args[start:stop].
This function is similar to instantiateRevRange, but it applies beta-reduction when
we instantiate a bound variable with a lambda expression.
Example: Given the term #0 a, and start := 0, stop := 1, args := #[fun x => x] the result is
a instead of (fun x => x) a.
This reduction is useful when we are inferring the type of eliminator-like applications.
For example, given (n m : Nat) (f : Nat → Nat) (h : m = n),
the type of Eq.subst (motive := fun x => f m = f x) h rfl
is motive n which is (fun (x : Nat) => f m = f x) n
This function reduces the new application to f m = f n
We use it to implement inferAppType
Instances For
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.inferTypeImp.infer (Lean.Expr.const c []) = Lean.Meta.inferConstType c []
- Lean.Meta.inferTypeImp.infer (Lean.Expr.const c us) = Lean.Meta.checkInferTypeCache (Lean.Expr.const c us) (Lean.Meta.inferConstType c us)
- Lean.Meta.inferTypeImp.infer (Lean.Expr.proj n i s) = Lean.Meta.checkInferTypeCache (Lean.Expr.proj n i s) (Lean.Meta.inferProjType n i s)
- Lean.Meta.inferTypeImp.infer (Lean.Expr.mvar mvarId) = Lean.Meta.inferMVarType mvarId
- Lean.Meta.inferTypeImp.infer (Lean.Expr.fvar fvarId) = Lean.Meta.inferFVarType fvarId
- Lean.Meta.inferTypeImp.infer (Lean.Expr.mdata data e_2) = Lean.Meta.inferTypeImp.infer e_2
- Lean.Meta.inferTypeImp.infer (Lean.Expr.lit v) = pure (Lean.Literal.type v)
- Lean.Meta.inferTypeImp.infer (Lean.Expr.sort lvl) = pure (Lean.mkSort (Lean.mkLevelSucc lvl))
Instances For
isPropQuick e is an "approximate" predicate which returns LBool.true
if e is a proposition.
isProp whnf e return true if e is a proposition.
If e contains metavariables, it may not be possible
to decide whether is a proposition or not. We return false in this
case. We considered using LBool and retuning LBool.undef, but
we have no applications for it.
Instances For
isProofQuick e is an "approximate" predicate which returns LBool.true
if e is a proof.
isTypeQuick e is an "approximate" predicate which returns LBool.true
if e is a type.
Return true iff the type of e is a Sort _.
Instances For
Equations
- Lean.Meta.isTypeFormerTypeQuick (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Meta.isTypeFormerTypeQuick b
- Lean.Meta.isTypeFormerTypeQuick (Lean.Expr.sort u) = true
- Lean.Meta.isTypeFormerTypeQuick x = false
Instances For
Return true iff type is Sort _ or As → Sort _.
Instances For
Return true iff e : Sort _ or e : (forall As, Sort _).
Remark: it subsumes isType