diff --git a/stage0/src/Init/Lean/Elab/Tactic.lean b/stage0/src/Init/Lean/Elab/Tactic.lean index 1133aca7ab..36c8df6ce9 100644 --- a/stage0/src/Init/Lean/Elab/Tactic.lean +++ b/stage0/src/Init/Lean/Elab/Tactic.lean @@ -7,3 +7,4 @@ prelude import Init.Lean.Elab.Term import Init.Lean.Elab.Tactic.Basic import Init.Lean.Elab.Tactic.ElabTerm +import Init.Lean.Elab.Tactic.Induction diff --git a/stage0/src/Init/Lean/Elab/Tactic/Induction.lean b/stage0/src/Init/Lean/Elab/Tactic/Induction.lean new file mode 100644 index 0000000000..7944cf2095 --- /dev/null +++ b/stage0/src/Init/Lean/Elab/Tactic/Induction.lean @@ -0,0 +1,19 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Sebastian Ullrich +-/ +prelude +import Init.Lean.Elab.Tactic.Basic + +namespace Lean +namespace Elab +namespace Tactic + +@[builtinTactic «induction»] def evalInduction : Tactic := +fun stx => focus stx $ + throwError stx ("WIP " ++ stx) + +end Tactic +end Elab +end Lean diff --git a/stage0/src/Init/Lean/Parser/Tactic.lean b/stage0/src/Init/Lean/Parser/Tactic.lean index d6ce54e95d..416518a992 100644 --- a/stage0/src/Init/Lean/Parser/Tactic.lean +++ b/stage0/src/Init/Lean/Parser/Tactic.lean @@ -36,6 +36,7 @@ def ident' : Parser := ident <|> underscore @[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticParser @[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip" @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState" +@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident def majorPremise := parser! optional (try (ident >> " : ")) >> termParser def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident >> many ident >> darrow >> termParser def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|") diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 28d9cc0f55..66061fa201 100644 --- a/stage0/stdlib/CMakeLists.txt +++ b/stage0/stdlib/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./MutQuot.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) +add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./HasCoe.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/Occurrences.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elab.c Init/./Lean/Elab/Alias.c Init/./Lean/Elab/App.c Init/./Lean/Elab/Binders.c Init/./Lean/Elab/BuiltinNotation.c Init/./Lean/Elab/Command.c Init/./Lean/Elab/DeclModifiers.c Init/./Lean/Elab/Declaration.c Init/./Lean/Elab/Definition.c Init/./Lean/Elab/DoNotation.c Init/./Lean/Elab/Exception.c Init/./Lean/Elab/Frontend.c Init/./Lean/Elab/Import.c Init/./Lean/Elab/Level.c Init/./Lean/Elab/Log.c Init/./Lean/Elab/Match.c Init/./Lean/Elab/Quotation.c Init/./Lean/Elab/ResolveName.c Init/./Lean/Elab/StrategyAttrs.c Init/./Lean/Elab/StructInst.c Init/./Lean/Elab/Syntax.c Init/./Lean/Elab/SyntheticMVars.c Init/./Lean/Elab/Tactic.c Init/./Lean/Elab/Tactic/Basic.c Init/./Lean/Elab/Tactic/ElabTerm.c Init/./Lean/Elab/Tactic/Induction.c Init/./Lean/Elab/Term.c Init/./Lean/Elab/Util.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Eval.c Init/./Lean/Expr.c Init/./Lean/HeadIndex.c Init/./Lean/Hygiene.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/KAbstract.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Message.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/RecursorInfo.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/Tactic.c Init/./Lean/Meta/Tactic/Apply.c Init/./Lean/Meta/Tactic/Assert.c Init/./Lean/Meta/Tactic/Assumption.c Init/./Lean/Meta/Tactic/Clear.c Init/./Lean/Meta/Tactic/FVarSubst.c Init/./Lean/Meta/Tactic/Generalize.c Init/./Lean/Meta/Tactic/Intro.c Init/./Lean/Meta/Tactic/LocalDecl.c Init/./Lean/Meta/Tactic/Revert.c Init/./Lean/Meta/Tactic/Rewrite.c Init/./Lean/Meta/Tactic/Subst.c Init/./Lean/Meta/Tactic/Target.c Init/./Lean/Meta/Tactic/Util.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Syntax.c Init/./Lean/Parser/Tactic.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Structure.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Util.c Init/./Lean/Util/CollectFVars.c Init/./Lean/Util/CollectLevelParams.c Init/./Lean/Util/CollectMVars.c Init/./Lean/Util/FindExpr.c Init/./Lean/Util/FindMVar.c Init/./Lean/Util/MonadCache.c Init/./Lean/Util/PPExt.c Init/./Lean/Util/PPGoal.c Init/./Lean/Util/Path.c Init/./Lean/Util/Profile.c Init/./Lean/Util/RecDepth.c Init/./Lean/Util/ReplaceExpr.c Init/./Lean/Util/Sorry.c Init/./Lean/Util/Trace.c Init/./Lean/Util/WHNF.c Init/./LeanInit.c Init/./MutQuot.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/IOError.c Init/./System/Platform.c Init/./Util.c Init/./WF.c) diff --git a/stage0/stdlib/Init/Lean/Elab/Tactic.c b/stage0/stdlib/Init/Lean/Elab/Tactic.c index ecf26603de..f61ecec663 100644 --- a/stage0/stdlib/Init/Lean/Elab/Tactic.c +++ b/stage0/stdlib/Init/Lean/Elab/Tactic.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Lean.Elab.Tactic -// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm +// Imports: Init.Lean.Elab.Term Init.Lean.Elab.Tactic.Basic Init.Lean.Elab.Tactic.ElabTerm Init.Lean.Elab.Tactic.Induction #include "runtime/lean.h" #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -16,6 +16,7 @@ extern "C" { lean_object* initialize_Init_Lean_Elab_Term(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*); lean_object* initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_object*); +lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object*); static bool _G_initialized = false; lean_object* initialize_Init_Lean_Elab_Tactic(lean_object* w) { lean_object * res; @@ -30,6 +31,9 @@ lean_dec_ref(res); res = initialize_Init_Lean_Elab_Tactic_ElabTerm(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Lean_Elab_Tactic_Induction(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Lean/Elab/Tactic/Induction.c b/stage0/stdlib/Init/Lean/Elab/Tactic/Induction.c new file mode 100644 index 0000000000..f0f208b1fc --- /dev/null +++ b/stage0/stdlib/Init/Lean/Elab/Tactic/Induction.c @@ -0,0 +1,142 @@ +// Lean compiler output +// Module: Init.Lean.Elab.Tactic.Induction +// Imports: Init.Lean.Elab.Tactic.Basic +#include "runtime/lean.h" +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +#ifdef __cplusplus +extern "C" { +#endif +lean_object* l_Lean_Elab_Tactic_evalInduction___closed__1; +lean_object* l_Lean_Elab_Tactic_evalInduction___closed__2; +extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3; +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3; +lean_object* l_Lean_Elab_Tactic_focus___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2; +lean_object* lean_name_mk_string(lean_object*, lean_object*); +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1; +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(lean_object*); +lean_object* l_Lean_Elab_Tactic_evalInduction___closed__3; +extern lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2; +lean_object* l_Lean_Elab_Tactic_evalInduction(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_addBuiltinTactic(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Tactic_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* _init_l_Lean_Elab_Tactic_evalInduction___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("WIP "); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Tactic_evalInduction___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_evalInduction___closed__1; +x_2 = lean_alloc_ctor(2, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Elab_Tactic_evalInduction___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_evalInduction___closed__2; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* l_Lean_Elab_Tactic_evalInduction(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; +lean_inc(x_1); +x_4 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_4, 0, x_1); +x_5 = l_Lean_Elab_Tactic_evalInduction___closed__3; +x_6 = lean_alloc_ctor(9, 2, 0); +lean_ctor_set(x_6, 0, x_5); +lean_ctor_set(x_6, 1, x_4); +lean_inc(x_1); +x_7 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_throwError___rarg), 4, 2); +lean_closure_set(x_7, 0, x_1); +lean_closure_set(x_7, 1, x_6); +x_8 = l_Lean_Elab_Tactic_focus___rarg(x_1, x_7, x_2, x_3); +return x_8; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("evalInduction"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3; +x_2 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction), 3, 0); +return x_1; +} +} +lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_Tactic_induction___elambda__1___closed__2; +x_3 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2; +x_4 = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3; +x_5 = l_Lean_Elab_Tactic_addBuiltinTactic(x_2, x_3, x_4, x_1); +return x_5; +} +} +lean_object* initialize_Init_Lean_Elab_Tactic_Basic(lean_object*); +static bool _G_initialized = false; +lean_object* initialize_Init_Lean_Elab_Tactic_Induction(lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_mk_io_result(lean_box(0)); +_G_initialized = true; +res = initialize_Init_Lean_Elab_Tactic_Basic(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Elab_Tactic_evalInduction___closed__1 = _init_l_Lean_Elab_Tactic_evalInduction___closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__1); +l_Lean_Elab_Tactic_evalInduction___closed__2 = _init_l_Lean_Elab_Tactic_evalInduction___closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__2); +l_Lean_Elab_Tactic_evalInduction___closed__3 = _init_l_Lean_Elab_Tactic_evalInduction___closed__3(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalInduction___closed__3); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__1); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__2); +l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3 = _init_l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3(); +lean_mark_persistent(l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction___closed__3); +res = l___regBuiltinTactic_Lean_Elab_Tactic_evalInduction(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +return lean_mk_io_result(lean_box(0)); +} +#ifdef __cplusplus +} +#endif diff --git a/stage0/stdlib/Init/Lean/Parser/Tactic.c b/stage0/stdlib/Init/Lean/Parser/Tactic.c index c349878062..5d424db267 100644 --- a/stage0/stdlib/Init/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Init/Lean/Parser/Tactic.c @@ -28,14 +28,17 @@ lean_object* l_Lean_Parser_Tactic_intros___closed__7; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_induction___closed__1; lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__8; extern lean_object* l_Lean_Parser_manyAux___main___closed__1; lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_revert___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___closed__1; lean_object* l_Lean_Parser_Tactic_case___closed__6; lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_mkError(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_apply___closed__2; lean_object* l_Lean_Parser_Tactic_clear___elambda__1___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___closed__2; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__5; extern lean_object* l_Lean_nullKind; @@ -45,11 +48,13 @@ lean_object* l_Lean_Parser_Tactic_orelse___closed__1; lean_object* l_Lean_Parser_Tactic_underscore___closed__2; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__4; extern lean_object* l_Lean_Parser_Tactic_seq___elambda__1___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___closed__6; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__1; lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__6; extern lean_object* l_Lean_Parser_Tactic_seq; lean_object* l_Lean_Parser_Tactic_skip___closed__3; lean_object* l_Lean_Parser_Tactic_induction___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___closed__4; lean_object* l_Lean_Parser_Tactic_generalizingVars___closed__5; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__1; @@ -105,6 +110,7 @@ lean_object* lean_array_get_size(lean_object*); lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__3; extern lean_object* l_Lean_Parser_Term_matchAlt___closed__7; lean_object* lean_string_append(lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Tactic_nestedTacticBlockCurly(lean_object*); lean_object* l_Lean_Parser_Tactic_subst___closed__4; @@ -112,6 +118,7 @@ lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__2; lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*); lean_object* l_Lean_Parser_Tactic_intros___closed__5; lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__2; +extern lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_usingRec; lean_object* l_Lean_Parser_Tactic_orelse___closed__3; lean_object* l_Lean_Parser_Tactic_clear___closed__4; @@ -120,6 +127,7 @@ lean_object* l_Lean_Parser_Tactic_revert___closed__1; lean_object* l_Lean_Parser_Tactic_skip___closed__1; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__5; lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_generalize___closed__3; lean_object* l_Lean_Parser_Tactic_orelse___closed__5; extern lean_object* l_Lean_Parser_Term_optIdent___closed__2; lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__8; @@ -144,6 +152,7 @@ lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_usingRec___closed__5; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__5; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -160,13 +169,16 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__10; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_clear___closed__3; lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__3; +lean_object* l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_object*); extern lean_object* l_Lean_Parser_identNoAntiquot___closed__1; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__3; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__12; lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_case___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_case; lean_object* l_Lean_Parser_Tactic_traceState___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__9; extern lean_object* l_Lean_Parser_ident___closed__2; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1(lean_object*, lean_object*); @@ -193,6 +205,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__7(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_revert; +lean_object* l_Lean_Parser_Tactic_generalize; lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__3; lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*); lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__7; @@ -204,6 +217,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_revert(lean_object*); lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__4(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object*); +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_traceState___closed__2; lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*); @@ -216,6 +230,7 @@ lean_object* l_Lean_Parser_Tactic_intros___closed__2; uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__7; lean_object* l_Lean_Parser_optionaInfo(lean_object*); +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_induction___closed__7; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_revert___closed__5; @@ -239,6 +254,7 @@ lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__1; extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__12; lean_object* l_Lean_Parser_Tactic_revert___closed__6; lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__11; lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_majorPremise___closed__3; extern lean_object* l_Lean_Parser_termParser___closed__2; @@ -248,6 +264,7 @@ lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__5; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__6; lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__7; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__10; lean_object* l_Lean_Parser_Tactic_majorPremise___closed__5; lean_object* l_Lean_Parser_Tactic_exact___closed__3; lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__3; @@ -288,12 +305,14 @@ lean_object* l_Lean_Parser_Tactic_apply; lean_object* l_Lean_Parser_Tactic_assumption___closed__5; lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_paren___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__10; lean_object* l_Lean_Parser_Tactic_paren___closed__2; lean_object* l_Lean_Parser_Tactic_subst___closed__3; lean_object* l_Lean_Parser_ParserState_popSyntax(lean_object*); lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__1; extern lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__5; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_case___closed__5; lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__2; @@ -301,6 +320,7 @@ lean_object* l_Lean_Parser_Tactic_orelse; lean_object* l_Lean_Parser_Tactic_allGoals___closed__6; lean_object* l_Lean_Parser_Tactic_subst___closed__5; lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_subst; lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__2; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Tactic_intros___elambda__1___spec__1(lean_object*, lean_object*); @@ -312,6 +332,7 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__6; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__6; extern lean_object* l___private_Init_Lean_Parser_Parser_11__antiquotNestedExpr___elambda__1___closed__7; extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__6; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__7; lean_object* l_Lean_Parser_nodeWithAntiquot(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__6(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_ident___elambda__1(lean_object*, lean_object*); @@ -332,6 +353,7 @@ lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_clear(lean_object*); lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__8; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_allGoals(lean_object*); lean_object* l_Lean_Parser_Tactic_induction___closed__6; lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*); @@ -366,6 +388,7 @@ extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11; lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__4; lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalizingVars___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__11; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_induction___closed__5; @@ -393,6 +416,7 @@ lean_object* l_Lean_Parser_Tactic_apply___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_assumption(lean_object*); extern lean_object* l_Lean_Parser_Term_matchAlts___closed__1; lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__2; +lean_object* l_Lean_Parser_Tactic_generalize___closed__7; lean_object* l_Lean_Parser_Tactic_induction___closed__4; extern lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__2; lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__2; @@ -434,6 +458,7 @@ lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_orelse___closed__6; lean_object* l_Lean_Parser_Tactic_intro___closed__5; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__1; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__12(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_skip(lean_object*); @@ -468,6 +493,7 @@ extern lean_object* l_Lean_Parser_Parser_inhabited___closed__1; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__3(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_refine; extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1; +lean_object* l_Lean_Parser_Tactic_generalize___closed__5; extern lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__6; lean_object* l_Lean_Parser_Tactic_seq___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__3; @@ -483,6 +509,7 @@ lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__4; lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__6; +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; lean_object* l_Lean_Parser_Tactic_traceState___elambda__1(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__14; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__4; @@ -4681,6 +4708,1358 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); return x_6; } } +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("generalize"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_seq___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__3; +x_3 = 1; +x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__1; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_eq___elambda__1___closed__3; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__7; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__8; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__10; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__12() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__8; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l_Lean_Parser_Tactic_generalize___elambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_3 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__4; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +lean_inc(x_2); +lean_inc(x_1); +x_5 = l_Lean_Parser_tryAnti(x_1, x_2); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; +lean_dec(x_4); +x_6 = lean_ctor_get(x_2, 0); +lean_inc(x_6); +x_7 = lean_array_get_size(x_6); +lean_dec(x_6); +x_42 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; +x_43 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__11; +lean_inc(x_1); +x_44 = l_Lean_Parser_nonReservedSymbolFnAux(x_42, x_43, x_1, x_2); +x_45 = lean_ctor_get(x_44, 3); +lean_inc(x_45); +if (lean_obj_tag(x_45) == 0) +{ +lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_72; lean_object* x_73; +x_46 = lean_ctor_get(x_44, 0); +lean_inc(x_46); +x_47 = lean_ctor_get(x_44, 1); +lean_inc(x_47); +x_48 = lean_array_get_size(x_46); +lean_dec(x_46); +lean_inc(x_1); +x_72 = l_Lean_Parser_ident___elambda__1(x_1, x_44); +x_73 = lean_ctor_get(x_72, 3); +lean_inc(x_73); +if (lean_obj_tag(x_73) == 0) +{ +lean_object* x_74; lean_object* x_75; lean_object* x_76; +x_74 = lean_ctor_get(x_72, 1); +lean_inc(x_74); +lean_inc(x_1); +x_75 = l_Lean_Parser_tokenFn(x_1, x_72); +x_76 = lean_ctor_get(x_75, 3); +lean_inc(x_76); +if (lean_obj_tag(x_76) == 0) +{ +lean_object* x_77; lean_object* x_78; +x_77 = lean_ctor_get(x_75, 0); +lean_inc(x_77); +x_78 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_77); +lean_dec(x_77); +if (lean_obj_tag(x_78) == 2) +{ +lean_object* x_79; lean_object* x_80; uint8_t x_81; +x_79 = lean_ctor_get(x_78, 1); +lean_inc(x_79); +lean_dec(x_78); +x_80 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__5; +x_81 = lean_string_dec_eq(x_79, x_80); +lean_dec(x_79); +if (x_81 == 0) +{ +lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; +x_82 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_83 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_82, x_74); +x_84 = lean_ctor_get(x_83, 0); +lean_inc(x_84); +x_85 = lean_ctor_get(x_83, 2); +lean_inc(x_85); +x_86 = lean_ctor_get(x_83, 3); +lean_inc(x_86); +x_49 = x_83; +x_50 = x_84; +x_51 = x_85; +x_52 = x_86; +goto block_71; +} +else +{ +lean_object* x_87; lean_object* x_88; lean_object* x_89; +lean_dec(x_74); +x_87 = lean_ctor_get(x_75, 0); +lean_inc(x_87); +x_88 = lean_ctor_get(x_75, 2); +lean_inc(x_88); +x_89 = lean_ctor_get(x_75, 3); +lean_inc(x_89); +x_49 = x_75; +x_50 = x_87; +x_51 = x_88; +x_52 = x_89; +goto block_71; +} +} +else +{ +lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; +lean_dec(x_78); +x_90 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_90, x_74); +x_92 = lean_ctor_get(x_91, 0); +lean_inc(x_92); +x_93 = lean_ctor_get(x_91, 2); +lean_inc(x_93); +x_94 = lean_ctor_get(x_91, 3); +lean_inc(x_94); +x_49 = x_91; +x_50 = x_92; +x_51 = x_93; +x_52 = x_94; +goto block_71; +} +} +else +{ +lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; +lean_dec(x_76); +x_95 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_96 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_95, x_74); +x_97 = lean_ctor_get(x_96, 0); +lean_inc(x_97); +x_98 = lean_ctor_get(x_96, 2); +lean_inc(x_98); +x_99 = lean_ctor_get(x_96, 3); +lean_inc(x_99); +x_49 = x_96; +x_50 = x_97; +x_51 = x_98; +x_52 = x_99; +goto block_71; +} +} +else +{ +lean_object* x_100; lean_object* x_101; lean_object* x_102; +lean_dec(x_73); +x_100 = lean_ctor_get(x_72, 0); +lean_inc(x_100); +x_101 = lean_ctor_get(x_72, 2); +lean_inc(x_101); +x_102 = lean_ctor_get(x_72, 3); +lean_inc(x_102); +x_49 = x_72; +x_50 = x_100; +x_51 = x_101; +x_52 = x_102; +goto block_71; +} +block_71: +{ +if (lean_obj_tag(x_52) == 0) +{ +lean_object* x_53; +lean_dec(x_51); +lean_dec(x_50); +x_53 = lean_ctor_get(x_49, 3); +lean_inc(x_53); +if (lean_obj_tag(x_53) == 0) +{ +lean_object* x_54; lean_object* x_55; +lean_dec(x_47); +x_54 = l_Lean_nullKind; +x_55 = l_Lean_Parser_ParserState_mkNode(x_49, x_54, x_48); +x_8 = x_55; +goto block_41; +} +else +{ +lean_object* x_56; uint8_t x_57; +lean_dec(x_53); +x_56 = lean_ctor_get(x_49, 1); +lean_inc(x_56); +x_57 = lean_nat_dec_eq(x_56, x_47); +lean_dec(x_56); +if (x_57 == 0) +{ +lean_object* x_58; lean_object* x_59; +lean_dec(x_47); +x_58 = l_Lean_nullKind; +x_59 = l_Lean_Parser_ParserState_mkNode(x_49, x_58, x_48); +x_8 = x_59; +goto block_41; +} +else +{ +lean_object* x_60; lean_object* x_61; lean_object* x_62; +x_60 = l_Lean_Parser_ParserState_restore(x_49, x_48, x_47); +x_61 = l_Lean_nullKind; +x_62 = l_Lean_Parser_ParserState_mkNode(x_60, x_61, x_48); +x_8 = x_62; +goto block_41; +} +} +} +else +{ +lean_object* x_63; lean_object* x_64; uint8_t x_65; +lean_dec(x_49); +x_63 = l_Array_shrink___main___rarg(x_50, x_48); +lean_inc(x_47); +x_64 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_64, 0, x_63); +lean_ctor_set(x_64, 1, x_47); +lean_ctor_set(x_64, 2, x_51); +lean_ctor_set(x_64, 3, x_52); +x_65 = lean_nat_dec_eq(x_47, x_47); +if (x_65 == 0) +{ +lean_object* x_66; lean_object* x_67; +lean_dec(x_47); +x_66 = l_Lean_nullKind; +x_67 = l_Lean_Parser_ParserState_mkNode(x_64, x_66, x_48); +x_8 = x_67; +goto block_41; +} +else +{ +lean_object* x_68; lean_object* x_69; lean_object* x_70; +x_68 = l_Lean_Parser_ParserState_restore(x_64, x_48, x_47); +x_69 = l_Lean_nullKind; +x_70 = l_Lean_Parser_ParserState_mkNode(x_68, x_69, x_48); +x_8 = x_70; +goto block_41; +} +} +} +} +else +{ +lean_object* x_103; lean_object* x_104; +lean_dec(x_45); +lean_dec(x_1); +x_103 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_104 = l_Lean_Parser_ParserState_mkNode(x_44, x_103, x_7); +return x_104; +} +block_41: +{ +lean_object* x_9; +x_9 = lean_ctor_get(x_8, 3); +lean_inc(x_9); +if (lean_obj_tag(x_9) == 0) +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_10 = l_Lean_Parser_termParser___closed__2; +x_11 = lean_unsigned_to_nat(50u); +lean_inc(x_1); +x_12 = l_Lean_Parser_categoryParser___elambda__1(x_10, x_11, x_1, x_8); +x_13 = lean_ctor_get(x_12, 3); +lean_inc(x_13); +if (lean_obj_tag(x_13) == 0) +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_14 = lean_ctor_get(x_12, 1); +lean_inc(x_14); +lean_inc(x_1); +x_15 = l_Lean_Parser_tokenFn(x_1, x_12); +x_16 = lean_ctor_get(x_15, 3); +lean_inc(x_16); +if (lean_obj_tag(x_16) == 0) +{ +lean_object* x_17; lean_object* x_18; +x_17 = lean_ctor_get(x_15, 0); +lean_inc(x_17); +x_18 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_17); +lean_dec(x_17); +if (lean_obj_tag(x_18) == 2) +{ +lean_object* x_19; lean_object* x_20; uint8_t x_21; +x_19 = lean_ctor_get(x_18, 1); +lean_inc(x_19); +lean_dec(x_18); +x_20 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_21 = lean_string_dec_eq(x_19, x_20); +lean_dec(x_19); +if (x_21 == 0) +{ +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; +lean_dec(x_1); +x_22 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_23 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_22, x_14); +x_24 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_7); +return x_25; +} +else +{ +lean_object* x_26; lean_object* x_27; lean_object* x_28; +lean_dec(x_14); +x_26 = l_Lean_Parser_ident___elambda__1(x_1, x_15); +x_27 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_7); +return x_28; +} +} +else +{ +lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; +lean_dec(x_18); +lean_dec(x_1); +x_29 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_29, x_14); +x_31 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_7); +return x_32; +} +} +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; +lean_dec(x_16); +lean_dec(x_1); +x_33 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_33, x_14); +x_35 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_7); +return x_36; +} +} +else +{ +lean_object* x_37; lean_object* x_38; +lean_dec(x_13); +lean_dec(x_1); +x_37 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_38 = l_Lean_Parser_ParserState_mkNode(x_12, x_37, x_7); +return x_38; +} +} +else +{ +lean_object* x_39; lean_object* x_40; +lean_dec(x_9); +lean_dec(x_1); +x_39 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_40 = l_Lean_Parser_ParserState_mkNode(x_8, x_39, x_7); +return x_40; +} +} +} +else +{ +lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; +x_105 = lean_ctor_get(x_2, 0); +lean_inc(x_105); +x_106 = lean_array_get_size(x_105); +lean_dec(x_105); +x_107 = lean_ctor_get(x_2, 1); +lean_inc(x_107); +lean_inc(x_1); +x_108 = lean_apply_2(x_4, x_1, x_2); +x_109 = lean_ctor_get(x_108, 3); +lean_inc(x_109); +if (lean_obj_tag(x_109) == 0) +{ +lean_dec(x_107); +lean_dec(x_106); +lean_dec(x_1); +return x_108; +} +else +{ +lean_object* x_110; lean_object* x_111; uint8_t x_112; +x_110 = lean_ctor_get(x_109, 0); +lean_inc(x_110); +lean_dec(x_109); +x_111 = lean_ctor_get(x_108, 1); +lean_inc(x_111); +x_112 = lean_nat_dec_eq(x_111, x_107); +lean_dec(x_111); +if (x_112 == 0) +{ +lean_dec(x_110); +lean_dec(x_107); +lean_dec(x_106); +lean_dec(x_1); +return x_108; +} +else +{ +lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; +lean_inc(x_107); +x_113 = l_Lean_Parser_ParserState_restore(x_108, x_106, x_107); +lean_dec(x_106); +x_114 = lean_ctor_get(x_113, 0); +lean_inc(x_114); +x_115 = lean_array_get_size(x_114); +lean_dec(x_114); +x_156 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; +x_157 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__11; +lean_inc(x_1); +x_158 = l_Lean_Parser_nonReservedSymbolFnAux(x_156, x_157, x_1, x_113); +x_159 = lean_ctor_get(x_158, 3); +lean_inc(x_159); +if (lean_obj_tag(x_159) == 0) +{ +lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; +x_160 = lean_ctor_get(x_158, 0); +lean_inc(x_160); +x_161 = lean_ctor_get(x_158, 1); +lean_inc(x_161); +x_162 = lean_array_get_size(x_160); +lean_dec(x_160); +lean_inc(x_1); +x_163 = l_Lean_Parser_ident___elambda__1(x_1, x_158); +x_164 = lean_ctor_get(x_163, 3); +lean_inc(x_164); +if (lean_obj_tag(x_164) == 0) +{ +lean_object* x_165; lean_object* x_166; lean_object* x_167; +x_165 = lean_ctor_get(x_163, 1); +lean_inc(x_165); +lean_inc(x_1); +x_166 = l_Lean_Parser_tokenFn(x_1, x_163); +x_167 = lean_ctor_get(x_166, 3); +lean_inc(x_167); +if (lean_obj_tag(x_167) == 0) +{ +lean_object* x_168; lean_object* x_169; +x_168 = lean_ctor_get(x_166, 0); +lean_inc(x_168); +x_169 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_168); +lean_dec(x_168); +if (lean_obj_tag(x_169) == 2) +{ +lean_object* x_170; lean_object* x_171; uint8_t x_172; +x_170 = lean_ctor_get(x_169, 1); +lean_inc(x_170); +lean_dec(x_169); +x_171 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__5; +x_172 = lean_string_dec_eq(x_170, x_171); +lean_dec(x_170); +if (x_172 == 0) +{ +lean_object* x_173; lean_object* x_174; uint8_t x_175; +x_173 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_174 = l_Lean_Parser_ParserState_mkErrorsAt(x_166, x_173, x_165); +x_175 = !lean_is_exclusive(x_174); +if (x_175 == 0) +{ +lean_object* x_176; lean_object* x_177; lean_object* x_178; uint8_t x_179; +x_176 = lean_ctor_get(x_174, 0); +x_177 = lean_ctor_get(x_174, 1); +lean_dec(x_177); +x_178 = l_Array_shrink___main___rarg(x_176, x_162); +lean_inc(x_161); +lean_ctor_set(x_174, 1, x_161); +lean_ctor_set(x_174, 0, x_178); +x_179 = lean_nat_dec_eq(x_161, x_161); +if (x_179 == 0) +{ +lean_object* x_180; lean_object* x_181; +lean_dec(x_161); +x_180 = l_Lean_nullKind; +x_181 = l_Lean_Parser_ParserState_mkNode(x_174, x_180, x_162); +x_116 = x_181; +goto block_155; +} +else +{ +lean_object* x_182; lean_object* x_183; lean_object* x_184; +x_182 = l_Lean_Parser_ParserState_restore(x_174, x_162, x_161); +x_183 = l_Lean_nullKind; +x_184 = l_Lean_Parser_ParserState_mkNode(x_182, x_183, x_162); +x_116 = x_184; +goto block_155; +} +} +else +{ +lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; uint8_t x_190; +x_185 = lean_ctor_get(x_174, 3); +x_186 = lean_ctor_get(x_174, 0); +x_187 = lean_ctor_get(x_174, 2); +lean_inc(x_185); +lean_inc(x_187); +lean_inc(x_186); +lean_dec(x_174); +x_188 = l_Array_shrink___main___rarg(x_186, x_162); +lean_inc(x_161); +x_189 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_189, 0, x_188); +lean_ctor_set(x_189, 1, x_161); +lean_ctor_set(x_189, 2, x_187); +lean_ctor_set(x_189, 3, x_185); +x_190 = lean_nat_dec_eq(x_161, x_161); +if (x_190 == 0) +{ +lean_object* x_191; lean_object* x_192; +lean_dec(x_161); +x_191 = l_Lean_nullKind; +x_192 = l_Lean_Parser_ParserState_mkNode(x_189, x_191, x_162); +x_116 = x_192; +goto block_155; +} +else +{ +lean_object* x_193; lean_object* x_194; lean_object* x_195; +x_193 = l_Lean_Parser_ParserState_restore(x_189, x_162, x_161); +x_194 = l_Lean_nullKind; +x_195 = l_Lean_Parser_ParserState_mkNode(x_193, x_194, x_162); +x_116 = x_195; +goto block_155; +} +} +} +else +{ +lean_object* x_196; +lean_dec(x_165); +x_196 = lean_ctor_get(x_166, 3); +lean_inc(x_196); +if (lean_obj_tag(x_196) == 0) +{ +lean_object* x_197; lean_object* x_198; lean_object* x_199; +lean_dec(x_161); +x_197 = l_Lean_nullKind; +x_198 = l_Lean_Parser_ParserState_mkNode(x_166, x_197, x_162); +x_199 = lean_ctor_get(x_198, 3); +lean_inc(x_199); +if (lean_obj_tag(x_199) == 0) +{ +lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; +x_200 = l_Lean_Parser_termParser___closed__2; +x_201 = lean_unsigned_to_nat(50u); +lean_inc(x_1); +x_202 = l_Lean_Parser_categoryParser___elambda__1(x_200, x_201, x_1, x_198); +x_203 = lean_ctor_get(x_202, 3); +lean_inc(x_203); +if (lean_obj_tag(x_203) == 0) +{ +lean_object* x_204; lean_object* x_205; lean_object* x_206; +x_204 = lean_ctor_get(x_202, 1); +lean_inc(x_204); +lean_inc(x_1); +x_205 = l_Lean_Parser_tokenFn(x_1, x_202); +x_206 = lean_ctor_get(x_205, 3); +lean_inc(x_206); +if (lean_obj_tag(x_206) == 0) +{ +lean_object* x_207; lean_object* x_208; +x_207 = lean_ctor_get(x_205, 0); +lean_inc(x_207); +x_208 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_207); +lean_dec(x_207); +if (lean_obj_tag(x_208) == 2) +{ +lean_object* x_209; lean_object* x_210; uint8_t x_211; +x_209 = lean_ctor_get(x_208, 1); +lean_inc(x_209); +lean_dec(x_208); +x_210 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_211 = lean_string_dec_eq(x_209, x_210); +lean_dec(x_209); +if (x_211 == 0) +{ +lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; +lean_dec(x_1); +x_212 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__12; +x_213 = l_Lean_Parser_ParserState_mkErrorsAt(x_205, x_212, x_204); +x_214 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_215 = l_Lean_Parser_ParserState_mkNode(x_213, x_214, x_115); +x_216 = l_Lean_Parser_mergeOrElseErrors(x_215, x_110, x_107); +lean_dec(x_107); +return x_216; +} +else +{ +lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; +lean_dec(x_204); +x_217 = l_Lean_Parser_ident___elambda__1(x_1, x_205); +x_218 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_219 = l_Lean_Parser_ParserState_mkNode(x_217, x_218, x_115); +x_220 = l_Lean_Parser_mergeOrElseErrors(x_219, x_110, x_107); +lean_dec(x_107); +return x_220; +} +} +else +{ +lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; +lean_dec(x_208); +lean_dec(x_1); +x_221 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__12; +x_222 = l_Lean_Parser_ParserState_mkErrorsAt(x_205, x_221, x_204); +x_223 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_224 = l_Lean_Parser_ParserState_mkNode(x_222, x_223, x_115); +x_225 = l_Lean_Parser_mergeOrElseErrors(x_224, x_110, x_107); +lean_dec(x_107); +return x_225; +} +} +else +{ +lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; +lean_dec(x_206); +lean_dec(x_1); +x_226 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__12; +x_227 = l_Lean_Parser_ParserState_mkErrorsAt(x_205, x_226, x_204); +x_228 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_229 = l_Lean_Parser_ParserState_mkNode(x_227, x_228, x_115); +x_230 = l_Lean_Parser_mergeOrElseErrors(x_229, x_110, x_107); +lean_dec(x_107); +return x_230; +} +} +else +{ +lean_object* x_231; lean_object* x_232; lean_object* x_233; +lean_dec(x_203); +lean_dec(x_1); +x_231 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_232 = l_Lean_Parser_ParserState_mkNode(x_202, x_231, x_115); +x_233 = l_Lean_Parser_mergeOrElseErrors(x_232, x_110, x_107); +lean_dec(x_107); +return x_233; +} +} +else +{ +lean_object* x_234; lean_object* x_235; lean_object* x_236; +lean_dec(x_199); +lean_dec(x_1); +x_234 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_235 = l_Lean_Parser_ParserState_mkNode(x_198, x_234, x_115); +x_236 = l_Lean_Parser_mergeOrElseErrors(x_235, x_110, x_107); +lean_dec(x_107); +return x_236; +} +} +else +{ +uint8_t x_237; +x_237 = !lean_is_exclusive(x_166); +if (x_237 == 0) +{ +lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; uint8_t x_242; +x_238 = lean_ctor_get(x_166, 0); +x_239 = lean_ctor_get(x_166, 3); +lean_dec(x_239); +x_240 = lean_ctor_get(x_166, 1); +lean_dec(x_240); +x_241 = l_Array_shrink___main___rarg(x_238, x_162); +lean_inc(x_161); +lean_ctor_set(x_166, 1, x_161); +lean_ctor_set(x_166, 0, x_241); +x_242 = lean_nat_dec_eq(x_161, x_161); +if (x_242 == 0) +{ +lean_object* x_243; lean_object* x_244; +lean_dec(x_161); +x_243 = l_Lean_nullKind; +x_244 = l_Lean_Parser_ParserState_mkNode(x_166, x_243, x_162); +x_116 = x_244; +goto block_155; +} +else +{ +lean_object* x_245; lean_object* x_246; lean_object* x_247; +x_245 = l_Lean_Parser_ParserState_restore(x_166, x_162, x_161); +x_246 = l_Lean_nullKind; +x_247 = l_Lean_Parser_ParserState_mkNode(x_245, x_246, x_162); +x_116 = x_247; +goto block_155; +} +} +else +{ +lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; uint8_t x_252; +x_248 = lean_ctor_get(x_166, 0); +x_249 = lean_ctor_get(x_166, 2); +lean_inc(x_249); +lean_inc(x_248); +lean_dec(x_166); +x_250 = l_Array_shrink___main___rarg(x_248, x_162); +lean_inc(x_161); +x_251 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_251, 0, x_250); +lean_ctor_set(x_251, 1, x_161); +lean_ctor_set(x_251, 2, x_249); +lean_ctor_set(x_251, 3, x_196); +x_252 = lean_nat_dec_eq(x_161, x_161); +if (x_252 == 0) +{ +lean_object* x_253; lean_object* x_254; +lean_dec(x_161); +x_253 = l_Lean_nullKind; +x_254 = l_Lean_Parser_ParserState_mkNode(x_251, x_253, x_162); +x_116 = x_254; +goto block_155; +} +else +{ +lean_object* x_255; lean_object* x_256; lean_object* x_257; +x_255 = l_Lean_Parser_ParserState_restore(x_251, x_162, x_161); +x_256 = l_Lean_nullKind; +x_257 = l_Lean_Parser_ParserState_mkNode(x_255, x_256, x_162); +x_116 = x_257; +goto block_155; +} +} +} +} +} +else +{ +lean_object* x_258; lean_object* x_259; uint8_t x_260; +lean_dec(x_169); +x_258 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_259 = l_Lean_Parser_ParserState_mkErrorsAt(x_166, x_258, x_165); +x_260 = !lean_is_exclusive(x_259); +if (x_260 == 0) +{ +lean_object* x_261; lean_object* x_262; lean_object* x_263; uint8_t x_264; +x_261 = lean_ctor_get(x_259, 0); +x_262 = lean_ctor_get(x_259, 1); +lean_dec(x_262); +x_263 = l_Array_shrink___main___rarg(x_261, x_162); +lean_inc(x_161); +lean_ctor_set(x_259, 1, x_161); +lean_ctor_set(x_259, 0, x_263); +x_264 = lean_nat_dec_eq(x_161, x_161); +if (x_264 == 0) +{ +lean_object* x_265; lean_object* x_266; +lean_dec(x_161); +x_265 = l_Lean_nullKind; +x_266 = l_Lean_Parser_ParserState_mkNode(x_259, x_265, x_162); +x_116 = x_266; +goto block_155; +} +else +{ +lean_object* x_267; lean_object* x_268; lean_object* x_269; +x_267 = l_Lean_Parser_ParserState_restore(x_259, x_162, x_161); +x_268 = l_Lean_nullKind; +x_269 = l_Lean_Parser_ParserState_mkNode(x_267, x_268, x_162); +x_116 = x_269; +goto block_155; +} +} +else +{ +lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; uint8_t x_275; +x_270 = lean_ctor_get(x_259, 3); +x_271 = lean_ctor_get(x_259, 0); +x_272 = lean_ctor_get(x_259, 2); +lean_inc(x_270); +lean_inc(x_272); +lean_inc(x_271); +lean_dec(x_259); +x_273 = l_Array_shrink___main___rarg(x_271, x_162); +lean_inc(x_161); +x_274 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_274, 0, x_273); +lean_ctor_set(x_274, 1, x_161); +lean_ctor_set(x_274, 2, x_272); +lean_ctor_set(x_274, 3, x_270); +x_275 = lean_nat_dec_eq(x_161, x_161); +if (x_275 == 0) +{ +lean_object* x_276; lean_object* x_277; +lean_dec(x_161); +x_276 = l_Lean_nullKind; +x_277 = l_Lean_Parser_ParserState_mkNode(x_274, x_276, x_162); +x_116 = x_277; +goto block_155; +} +else +{ +lean_object* x_278; lean_object* x_279; lean_object* x_280; +x_278 = l_Lean_Parser_ParserState_restore(x_274, x_162, x_161); +x_279 = l_Lean_nullKind; +x_280 = l_Lean_Parser_ParserState_mkNode(x_278, x_279, x_162); +x_116 = x_280; +goto block_155; +} +} +} +} +else +{ +lean_object* x_281; lean_object* x_282; uint8_t x_283; +lean_dec(x_167); +x_281 = l_Lean_Parser_Term_typeAscription___elambda__1___closed__8; +x_282 = l_Lean_Parser_ParserState_mkErrorsAt(x_166, x_281, x_165); +x_283 = !lean_is_exclusive(x_282); +if (x_283 == 0) +{ +lean_object* x_284; lean_object* x_285; lean_object* x_286; uint8_t x_287; +x_284 = lean_ctor_get(x_282, 0); +x_285 = lean_ctor_get(x_282, 1); +lean_dec(x_285); +x_286 = l_Array_shrink___main___rarg(x_284, x_162); +lean_inc(x_161); +lean_ctor_set(x_282, 1, x_161); +lean_ctor_set(x_282, 0, x_286); +x_287 = lean_nat_dec_eq(x_161, x_161); +if (x_287 == 0) +{ +lean_object* x_288; lean_object* x_289; +lean_dec(x_161); +x_288 = l_Lean_nullKind; +x_289 = l_Lean_Parser_ParserState_mkNode(x_282, x_288, x_162); +x_116 = x_289; +goto block_155; +} +else +{ +lean_object* x_290; lean_object* x_291; lean_object* x_292; +x_290 = l_Lean_Parser_ParserState_restore(x_282, x_162, x_161); +x_291 = l_Lean_nullKind; +x_292 = l_Lean_Parser_ParserState_mkNode(x_290, x_291, x_162); +x_116 = x_292; +goto block_155; +} +} +else +{ +lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; uint8_t x_298; +x_293 = lean_ctor_get(x_282, 3); +x_294 = lean_ctor_get(x_282, 0); +x_295 = lean_ctor_get(x_282, 2); +lean_inc(x_293); +lean_inc(x_295); +lean_inc(x_294); +lean_dec(x_282); +x_296 = l_Array_shrink___main___rarg(x_294, x_162); +lean_inc(x_161); +x_297 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_297, 0, x_296); +lean_ctor_set(x_297, 1, x_161); +lean_ctor_set(x_297, 2, x_295); +lean_ctor_set(x_297, 3, x_293); +x_298 = lean_nat_dec_eq(x_161, x_161); +if (x_298 == 0) +{ +lean_object* x_299; lean_object* x_300; +lean_dec(x_161); +x_299 = l_Lean_nullKind; +x_300 = l_Lean_Parser_ParserState_mkNode(x_297, x_299, x_162); +x_116 = x_300; +goto block_155; +} +else +{ +lean_object* x_301; lean_object* x_302; lean_object* x_303; +x_301 = l_Lean_Parser_ParserState_restore(x_297, x_162, x_161); +x_302 = l_Lean_nullKind; +x_303 = l_Lean_Parser_ParserState_mkNode(x_301, x_302, x_162); +x_116 = x_303; +goto block_155; +} +} +} +} +else +{ +lean_object* x_304; +lean_dec(x_164); +x_304 = lean_ctor_get(x_163, 3); +lean_inc(x_304); +if (lean_obj_tag(x_304) == 0) +{ +lean_object* x_305; uint8_t x_306; +x_305 = lean_ctor_get(x_163, 1); +lean_inc(x_305); +x_306 = lean_nat_dec_eq(x_305, x_161); +lean_dec(x_305); +if (x_306 == 0) +{ +lean_object* x_307; lean_object* x_308; +lean_dec(x_161); +x_307 = l_Lean_nullKind; +x_308 = l_Lean_Parser_ParserState_mkNode(x_163, x_307, x_162); +x_116 = x_308; +goto block_155; +} +else +{ +lean_object* x_309; lean_object* x_310; lean_object* x_311; +x_309 = l_Lean_Parser_ParserState_restore(x_163, x_162, x_161); +x_310 = l_Lean_nullKind; +x_311 = l_Lean_Parser_ParserState_mkNode(x_309, x_310, x_162); +x_116 = x_311; +goto block_155; +} +} +else +{ +uint8_t x_312; +x_312 = !lean_is_exclusive(x_163); +if (x_312 == 0) +{ +lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; uint8_t x_317; +x_313 = lean_ctor_get(x_163, 0); +x_314 = lean_ctor_get(x_163, 3); +lean_dec(x_314); +x_315 = lean_ctor_get(x_163, 1); +lean_dec(x_315); +x_316 = l_Array_shrink___main___rarg(x_313, x_162); +lean_inc(x_161); +lean_ctor_set(x_163, 1, x_161); +lean_ctor_set(x_163, 0, x_316); +x_317 = lean_nat_dec_eq(x_161, x_161); +if (x_317 == 0) +{ +lean_object* x_318; lean_object* x_319; +lean_dec(x_161); +x_318 = l_Lean_nullKind; +x_319 = l_Lean_Parser_ParserState_mkNode(x_163, x_318, x_162); +x_116 = x_319; +goto block_155; +} +else +{ +lean_object* x_320; lean_object* x_321; lean_object* x_322; +x_320 = l_Lean_Parser_ParserState_restore(x_163, x_162, x_161); +x_321 = l_Lean_nullKind; +x_322 = l_Lean_Parser_ParserState_mkNode(x_320, x_321, x_162); +x_116 = x_322; +goto block_155; +} +} +else +{ +lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; uint8_t x_327; +x_323 = lean_ctor_get(x_163, 0); +x_324 = lean_ctor_get(x_163, 2); +lean_inc(x_324); +lean_inc(x_323); +lean_dec(x_163); +x_325 = l_Array_shrink___main___rarg(x_323, x_162); +lean_inc(x_161); +x_326 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_326, 0, x_325); +lean_ctor_set(x_326, 1, x_161); +lean_ctor_set(x_326, 2, x_324); +lean_ctor_set(x_326, 3, x_304); +x_327 = lean_nat_dec_eq(x_161, x_161); +if (x_327 == 0) +{ +lean_object* x_328; lean_object* x_329; +lean_dec(x_161); +x_328 = l_Lean_nullKind; +x_329 = l_Lean_Parser_ParserState_mkNode(x_326, x_328, x_162); +x_116 = x_329; +goto block_155; +} +else +{ +lean_object* x_330; lean_object* x_331; lean_object* x_332; +x_330 = l_Lean_Parser_ParserState_restore(x_326, x_162, x_161); +x_331 = l_Lean_nullKind; +x_332 = l_Lean_Parser_ParserState_mkNode(x_330, x_331, x_162); +x_116 = x_332; +goto block_155; +} +} +} +} +} +else +{ +lean_object* x_333; lean_object* x_334; lean_object* x_335; +lean_dec(x_159); +lean_dec(x_1); +x_333 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_334 = l_Lean_Parser_ParserState_mkNode(x_158, x_333, x_115); +x_335 = l_Lean_Parser_mergeOrElseErrors(x_334, x_110, x_107); +lean_dec(x_107); +return x_335; +} +block_155: +{ +lean_object* x_117; +x_117 = lean_ctor_get(x_116, 3); +lean_inc(x_117); +if (lean_obj_tag(x_117) == 0) +{ +lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; +x_118 = l_Lean_Parser_termParser___closed__2; +x_119 = lean_unsigned_to_nat(50u); +lean_inc(x_1); +x_120 = l_Lean_Parser_categoryParser___elambda__1(x_118, x_119, x_1, x_116); +x_121 = lean_ctor_get(x_120, 3); +lean_inc(x_121); +if (lean_obj_tag(x_121) == 0) +{ +lean_object* x_122; lean_object* x_123; lean_object* x_124; +x_122 = lean_ctor_get(x_120, 1); +lean_inc(x_122); +lean_inc(x_1); +x_123 = l_Lean_Parser_tokenFn(x_1, x_120); +x_124 = lean_ctor_get(x_123, 3); +lean_inc(x_124); +if (lean_obj_tag(x_124) == 0) +{ +lean_object* x_125; lean_object* x_126; +x_125 = lean_ctor_get(x_123, 0); +lean_inc(x_125); +x_126 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_125); +lean_dec(x_125); +if (lean_obj_tag(x_126) == 2) +{ +lean_object* x_127; lean_object* x_128; uint8_t x_129; +x_127 = lean_ctor_get(x_126, 1); +lean_inc(x_127); +lean_dec(x_126); +x_128 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_129 = lean_string_dec_eq(x_127, x_128); +lean_dec(x_127); +if (x_129 == 0) +{ +lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; +lean_dec(x_1); +x_130 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_131 = l_Lean_Parser_ParserState_mkErrorsAt(x_123, x_130, x_122); +x_132 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_133 = l_Lean_Parser_ParserState_mkNode(x_131, x_132, x_115); +x_134 = l_Lean_Parser_mergeOrElseErrors(x_133, x_110, x_107); +lean_dec(x_107); +return x_134; +} +else +{ +lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; +lean_dec(x_122); +x_135 = l_Lean_Parser_ident___elambda__1(x_1, x_123); +x_136 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_137 = l_Lean_Parser_ParserState_mkNode(x_135, x_136, x_115); +x_138 = l_Lean_Parser_mergeOrElseErrors(x_137, x_110, x_107); +lean_dec(x_107); +return x_138; +} +} +else +{ +lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; +lean_dec(x_126); +lean_dec(x_1); +x_139 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_140 = l_Lean_Parser_ParserState_mkErrorsAt(x_123, x_139, x_122); +x_141 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_142 = l_Lean_Parser_ParserState_mkNode(x_140, x_141, x_115); +x_143 = l_Lean_Parser_mergeOrElseErrors(x_142, x_110, x_107); +lean_dec(x_107); +return x_143; +} +} +else +{ +lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; +lean_dec(x_124); +lean_dec(x_1); +x_144 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__9; +x_145 = l_Lean_Parser_ParserState_mkErrorsAt(x_123, x_144, x_122); +x_146 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_147 = l_Lean_Parser_ParserState_mkNode(x_145, x_146, x_115); +x_148 = l_Lean_Parser_mergeOrElseErrors(x_147, x_110, x_107); +lean_dec(x_107); +return x_148; +} +} +else +{ +lean_object* x_149; lean_object* x_150; lean_object* x_151; +lean_dec(x_121); +lean_dec(x_1); +x_149 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_150 = l_Lean_Parser_ParserState_mkNode(x_120, x_149, x_115); +x_151 = l_Lean_Parser_mergeOrElseErrors(x_150, x_110, x_107); +lean_dec(x_107); +return x_151; +} +} +else +{ +lean_object* x_152; lean_object* x_153; lean_object* x_154; +lean_dec(x_117); +lean_dec(x_1); +x_152 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_153 = l_Lean_Parser_ParserState_mkNode(x_116, x_152, x_115); +x_154 = l_Lean_Parser_mergeOrElseErrors(x_153, x_110, x_107); +lean_dec(x_107); +return x_154; +} +} +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__1() { +_start: +{ +lean_object* x_1; uint8_t x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__5; +x_2 = 0; +x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_termParser___closed__2; +x_2 = lean_unsigned_to_nat(50u); +x_3 = l_Lean_Parser_categoryParser(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__6; +x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_ident; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_generalize___closed__3; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_generalize___closed__2; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_generalize___closed__4; +x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_optIdent___closed__2; +x_2 = l_Lean_Parser_Tactic_generalize___closed__5; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___closed__1; +x_2 = l_Lean_Parser_Tactic_generalize___closed__6; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_generalize___closed__7; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_generalize___closed__8; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__10() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_generalize___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_generalize___closed__9; +x_2 = l_Lean_Parser_Tactic_generalize___closed__10; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_generalize() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Tactic_generalize___closed__11; +return x_1; +} +} +lean_object* l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; +x_2 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4; +x_3 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2; +x_4 = 1; +x_5 = l_Lean_Parser_Tactic_generalize; +x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} lean_object* _init_l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__1() { _start: { @@ -10821,6 +12200,57 @@ lean_mark_persistent(l_Lean_Parser_Tactic_traceState); res = l___regBuiltinParser_Lean_Parser_Tactic_traceState(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__1); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__2); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__3); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__4); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__5 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__5); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__6 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__6); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__7 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__7); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__8 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__8(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__8); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__9 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__9(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__9); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__10 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__10(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__10); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__11 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__11(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__11); +l_Lean_Parser_Tactic_generalize___elambda__1___closed__12 = _init_l_Lean_Parser_Tactic_generalize___elambda__1___closed__12(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___elambda__1___closed__12); +l_Lean_Parser_Tactic_generalize___closed__1 = _init_l_Lean_Parser_Tactic_generalize___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__1); +l_Lean_Parser_Tactic_generalize___closed__2 = _init_l_Lean_Parser_Tactic_generalize___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__2); +l_Lean_Parser_Tactic_generalize___closed__3 = _init_l_Lean_Parser_Tactic_generalize___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__3); +l_Lean_Parser_Tactic_generalize___closed__4 = _init_l_Lean_Parser_Tactic_generalize___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__4); +l_Lean_Parser_Tactic_generalize___closed__5 = _init_l_Lean_Parser_Tactic_generalize___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__5); +l_Lean_Parser_Tactic_generalize___closed__6 = _init_l_Lean_Parser_Tactic_generalize___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__6); +l_Lean_Parser_Tactic_generalize___closed__7 = _init_l_Lean_Parser_Tactic_generalize___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__7); +l_Lean_Parser_Tactic_generalize___closed__8 = _init_l_Lean_Parser_Tactic_generalize___closed__8(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__8); +l_Lean_Parser_Tactic_generalize___closed__9 = _init_l_Lean_Parser_Tactic_generalize___closed__9(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__9); +l_Lean_Parser_Tactic_generalize___closed__10 = _init_l_Lean_Parser_Tactic_generalize___closed__10(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__10); +l_Lean_Parser_Tactic_generalize___closed__11 = _init_l_Lean_Parser_Tactic_generalize___closed__11(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__11); +l_Lean_Parser_Tactic_generalize = _init_l_Lean_Parser_Tactic_generalize(); +lean_mark_persistent(l_Lean_Parser_Tactic_generalize); +res = l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__1); l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__2();