Equations
-
Lean.Elab.Term.elabAnonymousCtor stx expectedType? = let discr := stx;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.anonymousCtor = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let discr_2 := Lean.Syntax.getArg discr 1;
let discr := Lean.Syntax.getArg discr 2;
let args := { elemsAndSeps := Lean.Syntax.getArgs discr_2 };
do
Lean.Elab.Term.tryPostponeIfNoneOrMVar expectedType?
match expectedType? with
| some expectedType => do
let expectedType ← liftM (Lean.Meta.whnf expectedType)
Lean.matchConstInduct (Lean.Expr.getAppFn expectedType)
(fun x =>
Lean.throwError
(Lean.toMessageData "invalid constructor ⟨...⟩, expected type must be an inductive type " ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData ""))
fun ival us =>
match ival.ctors with
| [ctor] => do
let cinfo ← Lean.getConstInfoCtor ctor
let numExplicitFields ←
Lean.Meta.forallTelescopeReducing cinfo.toConstantVal.type fun xs x =>
let n := 0;
do
let r ←
let col := { start := cinfo.numParams, stop := Array.size xs, step := 1 };
forIn col n fun i r =>
let n := r;
do
let a ← liftM (Lean.Meta.getFVarLocalDecl (Array.getOp xs i))
if Lean.BinderInfo.isExplicit (Lean.LocalDecl.binderInfo a) = true then
let n := n + 1;
do
pure PUnit.unit
pure (ForInStep.yield n)
else do
pure PUnit.unit
pure (ForInStep.yield n)
let x : Nat := r
let n : Nat := x
pure n
let args : Array Lean.Syntax := Lean.Syntax.SepArray.getElems args
let _do_jp : PUnit → Lean.Elab.TermElabM Lean.Expr := fun y =>
let _do_jp := fun newStx =>
Lean.Elab.Term.withMacroExpansion stx newStx (Lean.Elab.Term.elabTerm newStx expectedType? true true);
if (Array.size args == numExplicitFields) = true then do
let y ←
do
let _ ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.mkCIdentFrom stx ctor,
Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] args)])
_do_jp y
else
if (numExplicitFields == 0) = true then do
let y ←
Lean.throwError
(Lean.toMessageData
"invalid constructor ⟨...⟩, insufficient number of arguments, constructs '" ++ Lean.toMessageData ctor ++ Lean.toMessageData "' does not have explicit fields, but #" ++ Lean.toMessageData (Array.size args) ++ Lean.toMessageData " provided")
_do_jp y
else
let extra := Array.toSubarray args (numExplicitFields - 1) (Array.size args);
do
let newLast ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.anonymousCtor
#[Lean.Syntax.atom info "⟨",
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(Lean.mkSepArray (Array.map (fun extra => extra) (Array.ofSubarray extra))
(Lean.mkAtom ","))),
Lean.Syntax.atom info "⟩"])
let newArgs : Array Lean.Syntax :=
Array.push (Subarray.toArray (Array.toSubarray args 0 (numExplicitFields - 1))) newLast
let y ←
do
let _ ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.mkCIdentFrom stx ctor,
Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] newArgs)])
_do_jp y
if Array.size args < numExplicitFields then do
let y ←
Lean.throwError
(Lean.toMessageData
"invalid constructor ⟨...⟩, insufficient number of arguments, constructs '" ++ Lean.toMessageData ctor ++ Lean.toMessageData "' has #" ++ Lean.toMessageData numExplicitFields ++ Lean.toMessageData " explicit fields, but only #" ++ Lean.toMessageData (Array.size args) ++ Lean.toMessageData " provided")
_do_jp y
else do
let y ← pure PUnit.unit
_do_jp y
| x =>
Lean.throwError
(Lean.toMessageData
"invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor " ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "")
| none => Lean.throwError (Lean.toMessageData "invalid constructor ⟨...⟩, expected type must be known")
else
let discr := stx;
Lean.Elab.throwUnsupportedSyntax
Equations
-
Lean.Elab.Term.expandShow stx = let discr := stx;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.show = 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;
if Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.fromTerm = true then
let discr := Lean.Syntax.getArg discr_3 0;
let discr := Lean.Syntax.getArg discr_3 1;
let val := discr;
let type := discr_2;
let thisId := Lean.mkIdentFrom stx `this;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun
#[Lean.Syntax.atom info "let_fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl
#[thisId, Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]],
Lean.Syntax.atom info ":=", val]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], thisId])
else
let discr_4 := Lean.Syntax.getArg discr 2;
if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.byTactic' = true then
let discr := Lean.Syntax.getArg discr_4 0;
let discr_5 := Lean.Syntax.getArg discr_4 1;
cond (Lean.Syntax.isOfKind discr_5 `Lean.Parser.Tactic.tacticSeq)
(let tac := discr_5;
let b := discr;
let type := discr_2;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.show
#[Lean.Syntax.atom info "show", type,
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fromTerm
#[Lean.Syntax.atom info "from",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic
#[Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? b) info) "by", tac]]]))
(let discr := Lean.Syntax.getArg discr_4 1;
Lean.Macro.throwUnsupported)
else
let discr := Lean.Syntax.getArg discr 2;
Lean.Macro.throwUnsupported
else
let discr := stx;
Lean.Macro.throwUnsupported
Equations
-
Lean.Elab.Term.expandHave stx = let thisId := Lean.mkIdentFrom stx `this;
let discr := stx;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.have = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let discr_2 := Lean.Syntax.getArg discr 1;
if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.haveDecl = true then
let discr_3 := Lean.Syntax.getArg discr_2 0;
if Lean.Syntax.isOfKind discr_3 `Lean.Parser.Term.haveIdDecl = true then
let discr_4 := Lean.Syntax.getArg discr_3 0;
if Lean.Syntax.matchesNull discr_4 2 = true then
let discr_5 := Lean.Syntax.getArg discr_4 0;
let discr_6 := Lean.Syntax.getArg discr_4 1;
let discr_7 := Lean.Syntax.getArg discr_3 1;
let yes := fun x type =>
let discr_8 := Lean.Syntax.getArg discr_3 2;
let discr_9 := Lean.Syntax.getArg discr_3 3;
let discr_10 := Lean.Syntax.getArg discr 2;
let yes := fun x =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let val := discr_9;
let bs := Lean.Syntax.getArgs discr_6;
let x := discr_5;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun
#[Lean.Syntax.atom info "let_fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl
#[x, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] bs),
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match type with
| some type =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]]
| none => Array.empty)),
Lean.Syntax.atom info ":=", val]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]);
if Lean.Syntax.isNone discr_10 = true then yes ()
else
let discr_11 := discr_10;
if Lean.Syntax.matchesNull discr_11 1 = true then
let discr := Lean.Syntax.getArg discr_11 0;
yes ()
else
let discr_12 := discr_10;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_7 = true then yes () none
else
let discr_8 := discr_7;
if Lean.Syntax.matchesNull discr_8 1 = true then
let discr_9 := Lean.Syntax.getArg discr_8 0;
if Lean.Syntax.isOfKind discr_9 `Lean.Parser.Term.typeSpec = true then
let discr := Lean.Syntax.getArg discr_9 0;
let discr := Lean.Syntax.getArg discr_9 1;
let type := discr;
yes () (some type)
else
let discr_10 := Lean.Syntax.getArg discr_8 0;
let discr_11 := Lean.Syntax.getArg discr_3 1;
let discr_12 := Lean.Syntax.getArg discr_3 2;
let discr_13 := Lean.Syntax.getArg discr_3 3;
let discr_14 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_9 := discr_7;
let discr_10 := Lean.Syntax.getArg discr_3 1;
let discr_11 := Lean.Syntax.getArg discr_3 2;
let discr_12 := Lean.Syntax.getArg discr_3 3;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_5 := Lean.Syntax.getArg discr_3 0;
if Lean.Syntax.matchesNull discr_5 0 = true then
let discr_6 := Lean.Syntax.getArg discr_3 1;
let yes := fun x type =>
let discr_7 := Lean.Syntax.getArg discr_3 2;
let discr_8 := Lean.Syntax.getArg discr_3 3;
let discr_9 := Lean.Syntax.getArg discr 2;
let yes := fun x =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let val := discr_8;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.have
#[Lean.Syntax.atom info "have",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveIdDecl
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[thisId, Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match type with
| some type =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]]
| none => Array.empty)),
Lean.Syntax.atom info ":=", val]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]);
if Lean.Syntax.isNone discr_9 = true then yes ()
else
let discr_10 := discr_9;
if Lean.Syntax.matchesNull discr_10 1 = true then
let discr := Lean.Syntax.getArg discr_10 0;
yes ()
else
let discr_11 := discr_9;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_6 = true then yes () none
else
let discr_7 := discr_6;
if Lean.Syntax.matchesNull discr_7 1 = true then
let discr_8 := Lean.Syntax.getArg discr_7 0;
if Lean.Syntax.isOfKind discr_8 `Lean.Parser.Term.typeSpec = true then
let discr := Lean.Syntax.getArg discr_8 0;
let discr := Lean.Syntax.getArg discr_8 1;
let type := discr;
yes () (some type)
else
let discr_9 := Lean.Syntax.getArg discr_7 0;
let discr_10 := Lean.Syntax.getArg discr_3 1;
let discr_11 := Lean.Syntax.getArg discr_3 2;
let discr_12 := Lean.Syntax.getArg discr_3 3;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_8 := discr_6;
let discr_9 := Lean.Syntax.getArg discr_3 1;
let discr_10 := Lean.Syntax.getArg discr_3 2;
let discr_11 := Lean.Syntax.getArg discr_3 3;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_6 := Lean.Syntax.getArg discr_3 0;
let discr_7 := Lean.Syntax.getArg discr_3 1;
let discr_8 := Lean.Syntax.getArg discr_3 2;
let discr_9 := Lean.Syntax.getArg discr_3 3;
let discr_10 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_4 := Lean.Syntax.getArg discr_2 0;
if Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.haveEqnsDecl = true then
let discr_5 := Lean.Syntax.getArg discr_4 0;
if Lean.Syntax.matchesNull discr_5 2 = true then
let discr_6 := Lean.Syntax.getArg discr_5 0;
let discr_7 := Lean.Syntax.getArg discr_5 1;
let discr_8 := Lean.Syntax.getArg discr_4 1;
let yes := fun x type =>
let discr_9 := Lean.Syntax.getArg discr_4 2;
cond (Lean.Syntax.isOfKind discr_9 `Lean.Parser.Term.matchAlts)
(let discr_10 := Lean.Syntax.getArg discr 2;
let yes := fun x =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let alts := discr_9;
let bs := Lean.Syntax.getArgs discr_7;
let x := discr_6;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun
#[Lean.Syntax.atom info "let_fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letEqnsDecl
#[x, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] bs),
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match type with
| some type =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]]
| none => Array.empty)),
alts]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]);
if Lean.Syntax.isNone discr_10 = true then yes ()
else
let discr_11 := discr_10;
if Lean.Syntax.matchesNull discr_11 1 = true then
let discr := Lean.Syntax.getArg discr_11 0;
yes ()
else
let discr_12 := discr_10;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported)
(let discr_10 := Lean.Syntax.getArg discr_4 2;
let discr_11 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported);
if Lean.Syntax.isNone discr_8 = true then yes () none
else
let discr_9 := discr_8;
if Lean.Syntax.matchesNull discr_9 1 = true then
let discr_10 := Lean.Syntax.getArg discr_9 0;
if Lean.Syntax.isOfKind discr_10 `Lean.Parser.Term.typeSpec = true then
let discr := Lean.Syntax.getArg discr_10 0;
let discr := Lean.Syntax.getArg discr_10 1;
let type := discr;
yes () (some type)
else
let discr_11 := Lean.Syntax.getArg discr_9 0;
let discr_12 := Lean.Syntax.getArg discr_4 1;
let discr_13 := Lean.Syntax.getArg discr_4 2;
let discr_14 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_10 := discr_8;
let discr_11 := Lean.Syntax.getArg discr_4 1;
let discr_12 := Lean.Syntax.getArg discr_4 2;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_6 := Lean.Syntax.getArg discr_4 0;
if Lean.Syntax.matchesNull discr_6 0 = true then
let discr_7 := Lean.Syntax.getArg discr_4 1;
let yes := fun x type =>
let discr_8 := Lean.Syntax.getArg discr_4 2;
cond (Lean.Syntax.isOfKind discr_8 `Lean.Parser.Term.matchAlts)
(let discr_9 := Lean.Syntax.getArg discr 2;
let yes := fun x =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let alts := discr_8;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.have
#[Lean.Syntax.atom info "have",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveEqnsDecl
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[thisId, Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match type with
| some type =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]]
| none => Array.empty)),
alts]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]);
if Lean.Syntax.isNone discr_9 = true then yes ()
else
let discr_10 := discr_9;
if Lean.Syntax.matchesNull discr_10 1 = true then
let discr := Lean.Syntax.getArg discr_10 0;
yes ()
else
let discr_11 := discr_9;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported)
(let discr_9 := Lean.Syntax.getArg discr_4 2;
let discr_10 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported);
if Lean.Syntax.isNone discr_7 = true then yes () none
else
let discr_8 := discr_7;
if Lean.Syntax.matchesNull discr_8 1 = true then
let discr_9 := Lean.Syntax.getArg discr_8 0;
if Lean.Syntax.isOfKind discr_9 `Lean.Parser.Term.typeSpec = true then
let discr := Lean.Syntax.getArg discr_9 0;
let discr := Lean.Syntax.getArg discr_9 1;
let type := discr;
yes () (some type)
else
let discr_10 := Lean.Syntax.getArg discr_8 0;
let discr_11 := Lean.Syntax.getArg discr_4 1;
let discr_12 := Lean.Syntax.getArg discr_4 2;
let discr_13 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_9 := discr_7;
let discr_10 := Lean.Syntax.getArg discr_4 1;
let discr_11 := Lean.Syntax.getArg discr_4 2;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_7 := Lean.Syntax.getArg discr_4 0;
let discr_8 := Lean.Syntax.getArg discr_4 1;
let discr_9 := Lean.Syntax.getArg discr_4 2;
let discr_10 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_5 := Lean.Syntax.getArg discr_2 0;
if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.letPatDecl = true then
let discr_6 := Lean.Syntax.getArg discr_5 0;
let discr_7 := Lean.Syntax.getArg discr_5 1;
if Lean.Syntax.matchesNull discr_7 0 = true then
let discr_8 := Lean.Syntax.getArg discr_5 2;
let yes := fun x type =>
let discr_9 := Lean.Syntax.getArg discr_5 3;
let discr_10 := Lean.Syntax.getArg discr_5 4;
let discr_11 := Lean.Syntax.getArg discr 2;
let yes := fun x =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let val := discr_10;
let pattern := discr_6;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun
#[Lean.Syntax.atom info "let_fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letPatDecl
#[pattern, Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match type with
| some type =>
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]]
| none => Array.empty)),
Lean.Syntax.atom info ":=", val]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], body]);
if Lean.Syntax.isNone discr_11 = true then yes ()
else
let discr_12 := discr_11;
if Lean.Syntax.matchesNull discr_12 1 = true then
let discr := Lean.Syntax.getArg discr_12 0;
yes ()
else
let discr_13 := discr_11;
let discr_14 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_8 = true then yes () none
else
let discr_9 := discr_8;
if Lean.Syntax.matchesNull discr_9 1 = true then
let discr_10 := Lean.Syntax.getArg discr_9 0;
if Lean.Syntax.isOfKind discr_10 `Lean.Parser.Term.typeSpec = true then
let discr := Lean.Syntax.getArg discr_10 0;
let discr := Lean.Syntax.getArg discr_10 1;
let type := discr;
yes () (some type)
else
let discr_11 := Lean.Syntax.getArg discr_9 0;
let discr_12 := Lean.Syntax.getArg discr_5 2;
let discr_13 := Lean.Syntax.getArg discr_5 3;
let discr_14 := Lean.Syntax.getArg discr_5 4;
let discr_15 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_10 := discr_8;
let discr_11 := Lean.Syntax.getArg discr_5 2;
let discr_12 := Lean.Syntax.getArg discr_5 3;
let discr_13 := Lean.Syntax.getArg discr_5 4;
let discr_14 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_8 := Lean.Syntax.getArg discr_5 1;
let discr_9 := Lean.Syntax.getArg discr_5 2;
let discr_10 := Lean.Syntax.getArg discr_5 3;
let discr_11 := Lean.Syntax.getArg discr_5 4;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_6 := Lean.Syntax.getArg discr_2 0;
let discr_7 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_3 := Lean.Syntax.getArg discr 1;
let discr_4 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr := stx;
Lean.Macro.throwUnsupported
Equations
-
Lean.Elab.Term.expandSuffices x = let discr := x;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.suffices = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let discr_2 := Lean.Syntax.getArg discr 1;
if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.sufficesDecl = true then
let discr_3 := Lean.Syntax.getArg discr_2 0;
let yes := fun x x =>
let discr_4 := Lean.Syntax.getArg discr_2 1;
let discr_5 := Lean.Syntax.getArg discr_2 2;
if Lean.Syntax.isOfKind discr_5 `Lean.Parser.Term.fromTerm = true then
let discr_6 := Lean.Syntax.getArg discr_5 0;
let discr_7 := Lean.Syntax.getArg discr_5 1;
let discr_8 := Lean.Syntax.getArg discr 2;
let yes := fun x_1 =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let val := discr_7;
let type := discr_4;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.have
#[Lean.Syntax.atom info "have",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveIdDecl
#[Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match x with
| some x => #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[]]
| none => Array.empty)),
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]],
Lean.Syntax.atom info ":=", body]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], val]);
if Lean.Syntax.isNone discr_8 = true then yes ()
else
let discr_9 := discr_8;
if Lean.Syntax.matchesNull discr_9 1 = true then
let discr := Lean.Syntax.getArg discr_9 0;
yes ()
else
let discr_10 := discr_8;
let discr_11 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_6 := Lean.Syntax.getArg discr_2 2;
if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Term.byTactic' = true then
let discr_7 := Lean.Syntax.getArg discr_6 0;
let discr_8 := Lean.Syntax.getArg discr_6 1;
cond (Lean.Syntax.isOfKind discr_8 `Lean.Parser.Tactic.tacticSeq)
(let discr_9 := Lean.Syntax.getArg discr 2;
let yes := fun x_1 =>
let discr := Lean.Syntax.getArg discr 3;
let body := discr;
let tac := discr_8;
let b := discr_7;
let type := discr_4;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.have
#[Lean.Syntax.atom info "have",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveDecl
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.haveIdDecl
#[Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match x with
| some x => #[x, Lean.Syntax.node Lean.SourceInfo.none `null #[]]
| none => Array.empty)),
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec
#[Lean.Syntax.atom info ":", type]],
Lean.Syntax.atom info ":=", body]],
Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic
#[Lean.Syntax.atom (Option.getD (Lean.Syntax.getHeadInfo? b) info) "by", tac]]);
if Lean.Syntax.isNone discr_9 = true then yes ()
else
let discr_10 := discr_9;
if Lean.Syntax.matchesNull discr_10 1 = true then
let discr := Lean.Syntax.getArg discr_10 0;
yes ()
else
let discr_11 := discr_9;
let discr_12 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported)
(let discr_9 := Lean.Syntax.getArg discr_6 1;
let discr_10 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported)
else
let discr_7 := Lean.Syntax.getArg discr_2 2;
let discr_8 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported;
if Lean.Syntax.isNone discr_3 = true then yes () none
else
let discr_4 := discr_3;
if Lean.Syntax.matchesNull discr_4 2 = true then
let discr := Lean.Syntax.getArg discr_4 0;
let discr_5 := Lean.Syntax.getArg discr_4 1;
let x := discr;
yes () (some x)
else
let discr_5 := discr_3;
let discr_6 := Lean.Syntax.getArg discr_2 0;
let discr_7 := Lean.Syntax.getArg discr_2 1;
let discr_8 := Lean.Syntax.getArg discr_2 2;
let discr_9 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr_3 := Lean.Syntax.getArg discr 1;
let discr_4 := Lean.Syntax.getArg discr 2;
let discr := Lean.Syntax.getArg discr 3;
Lean.Macro.throwUnsupported
else
let discr := x;
Lean.Macro.throwUnsupported
Equations
-
Lean.Elab.Term.elabPanic stx expectedType? = let arg := Lean.Syntax.getOp stx 1;
do
let pos ← Lean.Elab.getRefPosition
let env ← Lean.getEnv
let a ← Lean.Elab.Term.getDeclName?
let _do_jp : Lean.Syntax → Lean.Elab.TermElabM Lean.Expr := fun stxNew =>
Lean.Elab.Term.withMacroExpansion stx stxNew (Lean.Elab.Term.elabTerm stxNew expectedType? true true)
match a with
| some declName => do
let y ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "panicWithPosWithDecl")
(Lean.addMacroScope mainModule `panicWithPosWithDecl scp) [(`panicWithPosWithDecl, [])],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.quote (toString (Lean.Environment.mainModule env)), Lean.quote (toString declName),
Lean.quote pos.line, Lean.quote pos.column, arg]])
_do_jp y
| none => do
let y ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "panicWithPos")
(Lean.addMacroScope mainModule `panicWithPos scp) [(`panicWithPos, [])],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.quote (toString (Lean.Environment.mainModule env)), Lean.quote pos.line,
Lean.quote pos.column, arg]])
_do_jp y
Equations
-
Lean.Elab.Term.expandAssert stx = let cond := Lean.Syntax.getOp stx 1;
let body := Lean.Syntax.getOp stx 3;
match Lean.Syntax.reprint cond with
| some code => do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `termIfThenElse
#[Lean.Syntax.atom info "if", cond, Lean.Syntax.atom info "then", body, Lean.Syntax.atom info "else",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.panic
#[Lean.Syntax.atom info "panic!",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `«term_++_»
#[Lean.Syntax.node Lean.SourceInfo.none `strLit
#[Lean.Syntax.atom info "\"assertion violation: \""],
Lean.Syntax.atom info "++", Lean.quote code],
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"]]])
| none => do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `termIfThenElse
#[Lean.Syntax.atom info "if", cond, Lean.Syntax.atom info "then", body, Lean.Syntax.atom info "else",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.panic
#[Lean.Syntax.atom info "panic!",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `strLit
#[Lean.Syntax.atom info "\"assertion violation\""],
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"]]])
Equations
-
Lean.Elab.Term.expandDbgTrace stx = let arg := Lean.Syntax.getOp stx 1;
let body := Lean.Syntax.getOp stx 3;
if (Lean.Syntax.getKind arg == Lean.interpolatedStrKind) = true then do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "dbgTrace") (Lean.addMacroScope mainModule `dbgTrace scp)
[(`dbgTrace, [])],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `termS!_ #[Lean.Syntax.atom info "s!", arg],
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun
#[Lean.Syntax.atom info "fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]],
Lean.Syntax.atom info "=>", body]]]])
else do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "dbgTrace") (Lean.addMacroScope mainModule `dbgTrace scp)
[(`dbgTrace, [])],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app
#[Lean.Syntax.ident info (String.toSubstring "toString")
(Lean.addMacroScope mainModule `toString scp) [(`ToString.toString, [])],
Lean.Syntax.node Lean.SourceInfo.none `null #[arg]],
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun
#[Lean.Syntax.atom info "fun",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]],
Lean.Syntax.atom info "=>", body]]]])
Equations
-
Lean.Elab.Term.expandParen x = let discr := x;
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.paren = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let discr_2 := Lean.Syntax.getArg discr 1;
if Lean.Syntax.matchesNull discr_2 0 = true then
let discr := Lean.Syntax.getArg discr 2;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let scp ← Lean.getCurrMacroScope
let mainModule ← Lean.getMainModule
pure
(Lean.Syntax.ident info (String.toSubstring "Unit.unit") (Lean.addMacroScope mainModule `Unit.unit scp)
[(`Unit.unit, [])])
else
let discr_3 := Lean.Syntax.getArg discr 1;
if Lean.Syntax.matchesNull discr_3 2 = true then
let discr_4 := Lean.Syntax.getArg discr_3 0;
let discr_5 := Lean.Syntax.getArg discr_3 1;
if Lean.Syntax.matchesNull discr_5 1 = true then
let discr_6 := Lean.Syntax.getArg discr_5 0;
if Lean.Syntax.isOfKind discr_6 `Lean.Parser.Term.typeAscription = true then
let discr_7 := Lean.Syntax.getArg discr_6 0;
let discr_8 := Lean.Syntax.getArg discr_6 1;
let discr := Lean.Syntax.getArg discr 2;
let type := discr_8;
let e := discr_4;
do
let a ← Lean.Elab.Term.expandCDot? e
match a with
| some e => do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[e,
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription
#[Lean.Syntax.atom info ":", type]]],
Lean.Syntax.atom info ")"])
| none => Lean.Macro.throwUnsupported
else
let discr_7 := Lean.Syntax.getArg discr_5 0;
if Lean.Syntax.isOfKind discr_7 `Lean.Parser.Term.tupleTail = true then
let discr_8 := Lean.Syntax.getArg discr_7 0;
let discr_9 := Lean.Syntax.getArg discr_7 1;
let discr := Lean.Syntax.getArg discr 2;
let es := { elemsAndSeps := Lean.Syntax.getArgs discr_9 };
let e := discr_4;
do
let pairs ← Lean.Elab.Term.mkPairs (#[e] ++ Lean.Syntax.SepArray.getElems es)
let a ← Lean.Elab.Term.expandCDot? pairs
pure (Option.getD a pairs)
else
let discr_8 := Lean.Syntax.getArg discr_5 0;
let discr_9 := Lean.Syntax.getArg discr 2;
let stx := discr;
if
(!Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) && Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 1)) = true then
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0,
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"])
else throw (Lean.Macro.Exception.error stx "unexpected parentheses notation")
else
let discr_6 := Lean.Syntax.getArg discr_3 1;
if Lean.Syntax.matchesNull discr_6 0 = true then
let discr := Lean.Syntax.getArg discr 2;
let e := discr_4;
do
let a ← Lean.Elab.Term.expandCDot? e
pure (Option.getD a e)
else
let discr_7 := Lean.Syntax.getArg discr_3 1;
let discr_8 := Lean.Syntax.getArg discr 2;
let stx := discr;
if
(!Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) && Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 1)) = true then
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0,
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"])
else throw (Lean.Macro.Exception.error stx "unexpected parentheses notation")
else
let discr_4 := Lean.Syntax.getArg discr 1;
let discr_5 := Lean.Syntax.getArg discr 2;
let stx := discr;
if
(!Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) && Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 1)) = true then
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0, Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"])
else throw (Lean.Macro.Exception.error stx "unexpected parentheses notation")
else
let discr := x;
let stx := discr;
if
(!Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) && Lean.Syntax.isMissing (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 1)) = true then
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren
#[Lean.Syntax.atom info "(",
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0, Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.atom info ")"])
else throw (Lean.Macro.Exception.error stx "unexpected parentheses notation")
Equations
-
Lean.Elab.Term.elabSubst stx expectedType? = do
let expectedType ← Lean.Elab.Term.tryPostponeIfHasMVars expectedType? "invalid `▸` notation"
let discr : Lean.Syntax := stx
if Lean.Syntax.isOfKind discr `Lean.Parser.Term.subst = 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;
if Lean.Syntax.matchesNull discr_3 1 = true then
let discr := Lean.Syntax.getArg discr_3 0;
let hStx := discr;
let heqStx := discr_1;
do
let heq ← Lean.Elab.Term.elabTerm heqStx none true true
let heqType ← liftM (Lean.Meta.inferType heq)
let heqType ← liftM (Lean.Meta.instantiateMVars heqType)
let a ← liftM (Lean.Meta.matchEq? heqType)
match a with
| none =>
Lean.throwError
(Lean.toMessageData "invalid `▸` notation, argument" ++ Lean.toMessageData (Lean.indentExpr heq) ++ Lean.toMessageData "\nhas type" ++ Lean.toMessageData (Lean.indentExpr heqType) ++ Lean.toMessageData "\nequality expected")
| some (α, lhs, rhs) =>
let lhs := lhs;
let rhs := rhs;
let mkMotive := fun typeWithLooseBVar => do
let a ← liftM (Lean.mkFreshUserName `x)
Lean.Meta.withLocalDeclD a α fun x =>
liftM (Lean.Meta.mkLambdaFVars #[x] (Lean.Expr.instantiate1 typeWithLooseBVar x) false true);
do
let expectedAbst ← liftM (Lean.Meta.kabstract expectedType rhs Lean.Occurrences.all)
let _do_jp : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → PUnit → Lean.Elab.TermElabM Lean.Expr :=
fun lhs rhs heq expectedAbst y =>
let hExpectedType := Lean.Expr.instantiate1 expectedAbst lhs;
do
let discr ←
Lean.withRef hStx do
let h ← Lean.Elab.Term.elabTerm hStx (some hExpectedType) true true
let r ←
tryCatch
(do
let a ← Lean.Elab.Term.ensureHasType (some hExpectedType) h none
pure (a, none))
fun ex => do
let hType ← liftM (Lean.Meta.inferType h)
let hTypeAbst ← liftM (Lean.Meta.kabstract hType rhs Lean.Occurrences.all)
let _do_jp : PUnit → Lean.Elab.TermElabM (Lean.Expr × Option Lean.Expr) := fun y =>
let hTypeNew := Lean.Expr.instantiate1 hTypeAbst lhs;
do
let a ← liftM (Lean.Meta.isDefEq hExpectedType hTypeNew)
let _do_jp : PUnit → Lean.Elab.TermElabM (Lean.Expr × Option Lean.Expr) := fun y => do
let motive ← mkMotive hTypeAbst
let a ← liftM (Lean.Meta.isTypeCorrect motive)
if (!a) = true then pure (h, some motive)
else do
let a ← liftM (Lean.Meta.mkEqSymm heq)
let a ← liftM (Lean.Meta.mkEqNDRec motive h a)
pure (a, none)
if a = true then do
let y ← pure PUnit.unit
_do_jp y
else do
let y ← throw ex
_do_jp y
if Lean.Expr.hasLooseBVars hTypeAbst = true then do
let y ← pure PUnit.unit
_do_jp y
else do
let y ← throw ex
_do_jp y
pure r
let x : Lean.Expr × Option Lean.Expr := discr
match x with
| (h, badMotive?) => do
let motive ← mkMotive expectedAbst
let a ← liftM (Lean.Meta.isTypeCorrect motive)
if (Option.isSome badMotive? || !a) = true then do
let a ←
liftM (Lean.Elab.Term.isSubstCandidate lhs rhs) <||> liftM (Lean.Elab.Term.isSubstCandidate rhs lhs)
if a = true then
Lean.Elab.Term.withLocalIdentFor heqStx heq fun heqStx =>
Lean.Elab.Term.withLocalIdentFor hStx h fun hStx => do
let stxNew ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.byTactic
#[Lean.Syntax.atom info "by",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq
#[Lean.Syntax.node Lean.SourceInfo.none
`Lean.Parser.Tactic.tacticSeq1Indented
#[Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.node Lean.SourceInfo.none `group
#[Lean.Syntax.node Lean.SourceInfo.none
`Lean.Parser.Tactic.subst
#[Lean.Syntax.atom info "subst",
Lean.Syntax.node Lean.SourceInfo.none `null #[heqStx]],
Lean.Syntax.node Lean.SourceInfo.none `null
#[Lean.Syntax.atom info ";"]],
Lean.Syntax.node Lean.SourceInfo.none `group
#[Lean.Syntax.node Lean.SourceInfo.none
`Lean.Parser.Tactic.exact
#[Lean.Syntax.atom info "exact", hStx],
Lean.Syntax.node Lean.SourceInfo.none `null #[]]]]]])
Lean.Elab.Term.withMacroExpansion stx stxNew
(Lean.Elab.Term.elabTerm stxNew (some expectedType) true true)
else
Lean.throwError
(Lean.toMessageData "invalid `▸` notation, failed to compute motive for the substitution")
else liftM (Lean.Meta.mkEqNDRec motive h heq)
if Lean.Expr.hasLooseBVars expectedAbst = true then do
let y ← pure PUnit.unit
_do_jp lhs rhs heq expectedAbst y
else do
let r ← liftM (Lean.Meta.kabstract expectedType lhs Lean.Occurrences.all)
let expectedAbst : Lean.Expr := r
let _do_jp : Lean.Expr → Lean.Expr → Lean.Expr → PUnit → Lean.Elab.TermElabM Lean.Expr :=
fun lhs rhs heq y => do
let r ← liftM (Lean.Meta.mkEqSymm heq)
let heq : Lean.Expr := r
let x : Lean.Expr × Lean.Expr := (rhs, lhs)
match x with
| (lhs, rhs) => do
let y ← pure PUnit.unit
_do_jp lhs rhs heq expectedAbst y
if Lean.Expr.hasLooseBVars expectedAbst = true then do
let y ← pure PUnit.unit
_do_jp lhs rhs heq y
else do
let y ←
Lean.throwError
(Lean.toMessageData "invalid `▸` notation, expected type" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "\ndoes contain equation left-hand-side nor right-hand-side" ++ Lean.toMessageData (Lean.indentExpr heqType) ++ Lean.toMessageData "")
_do_jp lhs rhs heq y
else
let discr := Lean.Syntax.getArg discr 2;
Lean.Elab.throwUnsupportedSyntax
else
let discr := stx;
Lean.Elab.throwUnsupportedSyntax