Equations
-
Lean.Elab.Command.elabAuxDef x = let discr := x;
if Lean.Syntax.isOfKind discr `Lean.Elab.Command.aux_def = true then
let discr_1 := Lean.Syntax.getArg discr 0;
let yes := fun x doc? =>
let discr_2 := Lean.Syntax.getArg discr 1;
let yes := fun x attrs? =>
let discr_3 := Lean.Syntax.getArg discr 2;
let discr_4 := Lean.Syntax.getArg discr 3;
match
OptionM.run
(Array.sequenceMap (Lean.Syntax.getArgs discr_4) fun x =>
let discr := x;
cond (Lean.Syntax.isOfKind discr `ident)
(let suggestion := discr;
some suggestion)
(let discr := x;
none)) with
| some suggestion =>
let discr_5 := Lean.Syntax.getArg discr 4;
let discr_6 := Lean.Syntax.getArg discr 5;
let discr_7 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
let body := discr;
let ty := discr_6;
let id :=
Array.foldl (fun a a_1 => a ++ a_1) Lean.Name.anonymous
(Array.map (fun a => Lean.Name.eraseMacroScopes (Lean.Syntax.getId a)) suggestion) 0
(Array.size (Array.map (fun a => Lean.Name.eraseMacroScopes (Lean.Syntax.getId a)) suggestion));
do
let a ← Lean.getMainModule
let id : Lean.Name := `_aux ++ a ++ `_ ++ id
let id : String :=
String.intercalate "_" (List.map (fun a => Lean.Name.toString a false) (Lean.Name.components id))
let ns ← Lean.getCurrNamespace
let id ← Lean.mkAuxName (Lean.Name.mkStr ns id) 1
let id : Lean.Name := Lean.Name.replacePrefix id ns Lean.Name.anonymous
let a ←
do
let info ← Lean.MonadRef.mkInfoFromRefPos
let _ ← Lean.getCurrMacroScope
let _ ← Lean.getMainModule
pure
(Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declaration
#[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declModifiers
#[Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match doc? with
| some doc? => #[doc?]
| none => Array.empty)),
Lean.Syntax.node Lean.SourceInfo.none `null
(Array.append #[]
(match attrs? with
| some attrs? => #[attrs?]
| none => Array.empty)),
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.def
#[Lean.Syntax.atom info "def",
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declId
#[Lean.mkIdentFrom (Lean.mkNullNode suggestion) id,
Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.optDeclSig
#[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 ":", ty]]],
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Command.declValSimple
#[Lean.Syntax.atom info ":=", body, Lean.Syntax.node Lean.SourceInfo.none `null #[]],
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null #[],
Lean.Syntax.node Lean.SourceInfo.none `null #[]]])
Lean.Elab.Command.elabCommand a
| none =>
let discr_5 := Lean.Syntax.getArg discr 3;
let discr_6 := Lean.Syntax.getArg discr 4;
let discr_7 := Lean.Syntax.getArg discr 5;
let discr_8 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Elab.throwUnsupportedSyntax;
if Lean.Syntax.isNone discr_2 = true then yes () none
else
let discr_3 := discr_2;
if Lean.Syntax.matchesNull discr_3 1 = true then
let discr_4 := Lean.Syntax.getArg discr_3 0;
cond (Lean.Syntax.isOfKind discr_4 `Lean.Parser.Term.attributes)
(let attrs? := discr_4;
yes () (some attrs?))
(let discr_5 := Lean.Syntax.getArg discr_3 0;
let discr_6 := Lean.Syntax.getArg discr 1;
let discr_7 := Lean.Syntax.getArg discr 2;
let discr_8 := Lean.Syntax.getArg discr 3;
let discr_9 := Lean.Syntax.getArg discr 4;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Elab.throwUnsupportedSyntax)
else
let discr_4 := discr_2;
let discr_5 := Lean.Syntax.getArg discr 1;
let discr_6 := Lean.Syntax.getArg discr 2;
let discr_7 := Lean.Syntax.getArg discr 3;
let discr_8 := Lean.Syntax.getArg discr 4;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Elab.throwUnsupportedSyntax;
if Lean.Syntax.isNone discr_1 = true then yes () none
else
let discr_2 := discr_1;
if Lean.Syntax.matchesNull discr_2 1 = true then
let discr_3 := Lean.Syntax.getArg discr_2 0;
cond (Lean.Syntax.isOfKind discr_3 `Lean.Parser.Command.docComment)
(let doc? := discr_3;
yes () (some doc?))
(let discr_4 := Lean.Syntax.getArg discr_2 0;
let discr_5 := Lean.Syntax.getArg discr 0;
let discr_6 := Lean.Syntax.getArg discr 1;
let discr_7 := Lean.Syntax.getArg discr 2;
let discr_8 := Lean.Syntax.getArg discr 3;
let discr_9 := Lean.Syntax.getArg discr 4;
let discr_10 := Lean.Syntax.getArg discr 5;
let discr_11 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Elab.throwUnsupportedSyntax)
else
let discr_3 := discr_1;
let discr_4 := Lean.Syntax.getArg discr 0;
let discr_5 := Lean.Syntax.getArg discr 1;
let discr_6 := Lean.Syntax.getArg discr 2;
let discr_7 := Lean.Syntax.getArg discr 3;
let discr_8 := Lean.Syntax.getArg discr 4;
let discr_9 := Lean.Syntax.getArg discr 5;
let discr_10 := Lean.Syntax.getArg discr 6;
let discr := Lean.Syntax.getArg discr 7;
Lean.Elab.throwUnsupportedSyntax
else
let discr := x;
Lean.Elab.throwUnsupportedSyntax