Equations
- Lean.Elab.Term.hasElabWithoutExpectedType env declName = Lean.TagAttribute.hasTag Lean.Elab.Term.elabWithoutExpectedTypeAttr env declName
Equations
- Lean.Elab.Term.instToStringArg = { toString := fun x => match x with | Lean.Elab.Term.Arg.stx val => toString val | Lean.Elab.Term.Arg.expr val => toString val }
def
Lean.Elab.Term.throwInvalidNamedArg
{α : Type}
(namedArg : Lean.Elab.Term.NamedArg)
(fn? : Option Lean.Name)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
- explicit : Bool
- f : Lean.Expr
- fType : Lean.Expr
- args : List Lean.Elab.Term.Arg
- namedArgs : List Lean.Elab.Term.NamedArg
- ellipsis : Bool
- toSetErrorCtx : Array Lean.MVarId
- instMVars : Array Lean.MVarId
- propagateExpected : Bool
@[inline]
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Elab.Term.ElabAppArgs.eraseNamedArgCore
(namedArgs : List Lean.Elab.Term.NamedArg)
(binderName : Lean.Name)
:
Equations
- Lean.Elab.Term.ElabAppArgs.eraseNamedArgCore namedArgs binderName = List.filter (fun a => a.name != binderName) namedArgs
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Elab.Term.elabAppArgs
(f : Lean.Expr)
(namedArgs : Array Lean.Elab.Term.NamedArg)
(args : Array Lean.Elab.Term.Arg)
(expectedType? : Option Lean.Expr)
(explicit : Bool)
(ellipsis : Bool)
:
Equations
- One or more equations did not get rendered due to their size.
- projFn: Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Term.LValResolution
- projIdx: Lean.Name → Nat → Lean.Elab.Term.LValResolution
- const: Lean.Name → Lean.Name → Lean.Name → Lean.Elab.Term.LValResolution
- localRec: Lean.Name → Lean.Name → Lean.Expr → Lean.Elab.Term.LValResolution
- getOp: Lean.Name → Lean.Syntax → Lean.Elab.Term.LValResolution
Auxiliary inductive datatype that represents the resolution of an LVal.
Equations
- Lean.Elab.Term.elabExplicitUnivs lvls = Array.foldrM (fun stx lvls => do let a ← Lean.Elab.Term.elabLevel stx pure (a :: lvls)) [] lvls (Array.size lvls)
Equations
- One or more equations did not get rendered due to their size.
x@e matches the pattern e and binds its value to the identifier x.
x.{u, ...} explicitly specifies the universes u, ... of the constant x.
e |>.x is a shorthand for (e).x. It is especially useful for avoiding parentheses with repeated applications.
Equations
- One or more equations did not get rendered due to their size.
@x disables automatic insertion of implicit parameters of the constant x.
@e for any term e also disables the insertion of implicit lambdas at this position.
Equations
- One or more equations did not get rendered due to their size.