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
- Lean.Elab.Term.throwInvalidNamedArg namedArg fn? = Lean.withRef namedArg.ref (match fn? with | some fn => Lean.throwError (Lean.toMessageData "invalid argument name '" ++ Lean.toMessageData namedArg.name ++ Lean.toMessageData "' for function '" ++ Lean.toMessageData fn ++ Lean.toMessageData "'") | none => Lean.throwError (Lean.toMessageData "invalid argument name '" ++ Lean.toMessageData namedArg.name ++ Lean.toMessageData "' for function"))
Equations
- Lean.Elab.Term.synthesizeAppInstMVars instMVars app = do let r ← forIn instMVars PUnit.unit fun mvarId r => do let a ← Lean.Elab.Term.synthesizeInstMVarCore mvarId none if a = true then do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do Lean.Elab.Term.registerSyntheticMVarWithCurrRef mvarId Lean.Elab.Term.SyntheticMVarKind.typeClass let a ← Lean.getRef Lean.Elab.Term.registerMVarErrorImplicitArgInfo mvarId a app pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
- explicit : Bool
- f : Lean.Expr
- fType : Lean.Expr
- args : List Lean.Elab.Term.Arg
- namedArgs : List Lean.Elab.Term.NamedArg
- ellipsis : Bool
- expectedType? : Option Lean.Expr
- etaArgs : Array Lean.Expr
- toSetErrorCtx : Array Lean.MVarId
- instMVars : Array Lean.MVarId
- propagateExpected : Bool
@[inline]
Equations
- Lean.Elab.Term.ElabAppArgs.synthesizeAppInstMVars = do let s ← get let instMVars : Array Lean.MVarId := s.instMVars modify fun s => { explicit := s.explicit, f := s.f, fType := s.fType, args := s.args, namedArgs := s.namedArgs, ellipsis := s.ellipsis, expectedType? := s.expectedType?, etaArgs := s.etaArgs, toSetErrorCtx := s.toSetErrorCtx, instMVars := #[], propagateExpected := s.propagateExpected } liftM (Lean.Elab.Term.synthesizeAppInstMVars instMVars s.f)
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
- Lean.Elab.Term.ElabAppArgs.eraseNamedArg binderName = modify fun s => { explicit := s.explicit, f := s.f, fType := s.fType, args := s.args, namedArgs := Lean.Elab.Term.ElabAppArgs.eraseNamedArgCore s.namedArgs binderName, ellipsis := s.ellipsis, expectedType? := s.expectedType?, etaArgs := s.etaArgs, toSetErrorCtx := s.toSetErrorCtx, instMVars := s.instMVars, propagateExpected := s.propagateExpected }
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
- Lean.Elab.Term.elabAppArgs f namedArgs args expectedType? explicit ellipsis = do let fType ← liftM (Lean.Meta.inferType f) let fType ← liftM (Lean.Meta.instantiateMVars fType) let cls : Lean.Name := `Elab.app.args let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => let _do_jp := fun y => do let a ← Lean.Elab.Term.propagateExpectedTypeFor f StateRefT'.run' Lean.Elab.Term.ElabAppArgs.main { explicit := explicit, f := f, fType := fType, args := Array.toList args, namedArgs := Array.toList namedArgs, ellipsis := ellipsis, expectedType? := expectedType?, etaArgs := #[], toSetErrorCtx := #[], instMVars := #[], propagateExpected := a }; if (Array.isEmpty namedArgs && Array.isEmpty args) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Elab.Term.tryPostponeIfMVar fType _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "explicit: " ++ Lean.toMessageData explicit ++ Lean.toMessageData ", " ++ Lean.toMessageData f ++ Lean.toMessageData " : " ++ Lean.toMessageData fType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
- 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
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
- Lean.Elab.Term.elabApp stx expectedType? = Lean.Elab.Term.withoutPostponingUniverseConstraints do let discr ← Lean.Elab.Term.expandApp stx false let x : Lean.Syntax × Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool := discr match x with | (f, namedArgs, args, ellipsis) => do let result ← Lean.Elab.Term.elabAppAux f namedArgs args ellipsis expectedType? let resultFn : Lean.Expr := Lean.Expr.getAppFn result let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Expr := fun y => pure result if Lean.Expr.isFVar resultFn = true then do let localDecl ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! resultFn)) if Lean.LocalDecl.isAuxDecl localDecl = true then pure (Lean.mkRecAppWithSyntax result stx) else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Elab.Term.elabPipeProj x x = let discr := x; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.pipeProj = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let discr_4 := x; let expectedType? := discr_4; let args := Lean.Syntax.getArgs discr; let f := discr_3; let e := discr_1; Lean.Elab.Term.withoutPostponingUniverseConstraints do let discr ← Lean.Elab.Term.expandArgs args false let x : Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool := discr match x with | (namedArgs, args, ellipsis) => do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.pipeProj #[e, Lean.Syntax.atom info "|>.", f, Lean.Syntax.node Lean.SourceInfo.none `null #[]]) Lean.Elab.Term.elabAppAux a namedArgs args ellipsis expectedType? else let discr := x; let discr := x; Lean.Elab.throwUnsupportedSyntax
Equations
- Lean.Elab.Term.elabExplicit stx expectedType? = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.explicit = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; cond (Lean.Syntax.isOfKind discr_2 `ident) (let id := discr_2; Lean.Elab.Term.elabAtom stx expectedType?) (let discr_3 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.explicitUniv = true then let discr := Lean.Syntax.getArg discr_3 0; cond (Lean.Syntax.isOfKind discr `ident) (let discr_4 := Lean.Syntax.getArg discr_3 1; let discr_5 := Lean.Syntax.getArg discr_3 2; let discr_6 := Lean.Syntax.getArg discr_3 3; let us := { elemsAndSeps := Lean.Syntax.getArgs discr_5 }; let id := discr; Lean.Elab.Term.elabAtom stx expectedType?) (let discr := Lean.Syntax.getArg discr_3 0; let discr := Lean.Syntax.getArg discr_3 1; let discr := Lean.Syntax.getArg discr_3 2; let discr := Lean.Syntax.getArg discr_3 3; let t := discr_3; Lean.Elab.Term.elabTerm t expectedType? true false) else let discr_4 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.paren = true then let discr := Lean.Syntax.getArg discr_4 0; let discr := Lean.Syntax.getArg discr_4 1; if Lean.Syntax.matchesNull discr 2 = true then let discr_5 := Lean.Syntax.getArg discr 0; let discr_6 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_6 0 = true then let discr := Lean.Syntax.getArg discr_4 2; let t := discr_5; Lean.Elab.Term.elabTerm t expectedType? true false else let discr := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr_4 2; let t := discr_4; Lean.Elab.Term.elabTerm t expectedType? true false else let discr := Lean.Syntax.getArg discr_4 1; let discr := Lean.Syntax.getArg discr_4 2; let t := discr_4; Lean.Elab.Term.elabTerm t expectedType? true false else let discr := Lean.Syntax.getArg discr 1; let t := discr; Lean.Elab.Term.elabTerm t expectedType? true false) else let discr := stx; Lean.Elab.throwUnsupportedSyntax