max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-02 19:49:31 -07:00
parent 95b83ac2c0
commit d803a6787a
23 changed files with 4603 additions and 1069 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
stage0/src/Init/Conv.lean generated
View file

@ -18,24 +18,27 @@ syntax convSeq := convSeq1Indented <|> convSeqBracketed
syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
syntax (name := skip) "skip " : conv
syntax (name := skip) "skip" : conv
syntax (name := done) "done" : conv
syntax (name := lhs) "lhs" : conv
syntax (name := rhs) "rhs" : conv
syntax (name := whnf) "whnf" : conv
syntax (name := congr) "congr" : conv
syntax (name := arg) "arg " num : conv
syntax (name := trace) "trace" : conv
syntax (name := traceState) "traceState" : conv
syntax (name := funext) "funext" ident* : conv
syntax (name := change) "change " term : conv
syntax (name := rewrite) "rewrite " rwRuleSeq : conv
syntax (name := erewrite) "erewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := nestedTactic) "tactic " tacticSeq : conv
syntax (name := nestedTactic) "tactic" " => " tacticSeq : conv
syntax (name := nestedConv) convSeqBracketed : conv
syntax (name := paren) "(" convSeq ")" : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
macro "erw " s:rwRuleSeq : conv => `(erewrite $s:rwRuleSeq)
macro "args" : conv => `(congr)
macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)

2
stage0/src/Lean/Elab/Tactic/Conv.lean generated
View file

@ -5,3 +5,5 @@ Authors: Leonardo de Moura
-/
import Lean.Elab.Tactic.Conv.Basic
import Lean.Elab.Tactic.Conv.Congr
import Lean.Elab.Tactic.Conv.Rewrite
import Lean.Elab.Tactic.Conv.Change

33
stage0/src/Lean/Elab/Tactic/Conv/Basic.lean generated
View file

@ -87,16 +87,41 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
@[builtinTactic Lean.Parser.Tactic.Conv.paren] def evalParen : Tactic := fun stx =>
evalTactic stx[1]
private def convTarget (conv : Syntax) : TacticM Unit := do
@[builtinTactic Lean.Parser.Tactic.Conv.done] def evalDone : Tactic := fun _ =>
done
@[builtinTactic Lean.Parser.Tactic.Conv.traceState] def evalTraceState : Tactic :=
Tactic.evalTraceState
@[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
let seq := stx[2]
let target ← getMainTarget
if let some _ := isLHSGoal? target then
liftMetaTactic1 fun mvarId =>
replaceTargetDefEq mvarId target.mdataExpr!
focus <| evalTactic seq
private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
let target ← getMainTarget
let (targetNew, proof) ← convert target (evalTactic conv)
liftMetaTactic1 fun mvarId => replaceTargetEq mvarId targetNew proof
private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do
let localDecl ← getLocalDeclFromUserName hUserName
let (typeNew, proof) ← convert localDecl.type (evalTactic conv)
liftMetaTactic1 fun mvarId =>
return some (← replaceLocalDecl mvarId localDecl.fvarId typeNew proof).mvarId
@[builtinTactic Lean.Parser.Tactic.Conv.conv] def evalConv : Tactic := fun stx => do
match stx with
| `(tactic| conv $[at $loc]? $[in $e]? => $code) =>
-- TODO: implement `at` and `in` support
convTarget code
| `(tactic| conv $[at $loc?]? $[in $e?]? => $code) =>
-- TODO: implement `at` support
unless e?.isNone do
throwError "'in' modifier has not been implemented yet"
if let some loc := loc? then
convLocalDecl code loc.getId
else
convTarget code
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Conv

24
stage0/src/Lean/Elab/Tactic/Conv/Change.lean generated Normal file
View file

@ -0,0 +1,24 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Tactic.ElabTerm
import Lean.Elab.Tactic.Conv.Basic
namespace Lean.Elab.Tactic.Conv
open Meta
@[builtinTactic Lean.Parser.Tactic.Conv.change] def evalChange : Tactic := fun stx => do
match stx with
| `(conv| change $e) => do
let lhs ← getLhs
let mvarCounterSaved := (← getMCtx).mvarCounter
let r ← elabTermEnsuringType e (← inferType lhs)
logUnassignedAndAbort (← filterOldMVars (← getMVars r) mvarCounterSaved)
unless (← isDefEqGuarded r lhs) do
throwError "invalid 'change' conv tactic, term{indentExpr r}\nis not definitionally equal to current left-hand-side{indentExpr lhs}"
changeLhs r
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Conv

18
stage0/src/Lean/Elab/Tactic/Conv/Congr.lean generated
View file

@ -52,4 +52,22 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) :=
applyRefl mvarId₁
replaceMainGoal [mvarId₂]
@[builtinTactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
match stx with
| `(conv| arg $i) =>
let i := i.isNatLit?.getD 0
if i == 0 then
throwError "invalid 'arg' conv tactic, index must be greater than 0"
let i := i - 1
let mvarIds ← congr (← getMainGoal)
if h : i < mvarIds.length then
for mvarId in mvarIds, j in [:mvarIds.length] do
if i != j then
applyRefl mvarId
replaceMainGoal [mvarIds.get i h]
else
throwError "invalid 'arg' conv tactic, application has only {mvarIds.length} (nondependent) arguments"
| _ => throwUnsupportedSyntax
end Lean.Elab.Tactic.Conv

27
stage0/src/Lean/Elab/Tactic/Conv/Rewrite.lean generated Normal file
View file

@ -0,0 +1,27 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Rewrite
import Lean.Elab.Tactic.Rewrite
import Lean.Elab.Tactic.Conv.Basic
namespace Lean.Elab.Tactic.Conv
open Meta
def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx =>
withRWRulesSeq stx[0] stx[1] fun symm term => do
Term.withSynthesize <| withMainContext do
let e ← elabTerm term none true
let r ← rewrite (← getMainGoal) (← getLhs) e symm (mode := mode)
updateLhs r.eNew r.eqProof
replaceMainGoal ((← getMainGoal) :: r.mvarIds)
@[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic :=
evalRewriteCore TransparencyMode.instances
@[builtinTactic Lean.Parser.Tactic.Conv.erewrite] def evalERewrite : Tactic :=
evalRewriteCore TransparencyMode.default
end Lean.Elab.Tactic.Conv

4
stage0/src/Lean/Elab/Tactic/ElabTerm.lean generated
View file

@ -43,11 +43,11 @@ def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : T
withMainContext do
closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget))
private def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do
if (← Term.logUnassignedUsingErrorInfos mvarIds) then
throwAbortTactic
private def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Array MVarId) := do
def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Array MVarId) := do
let mctx ← getMCtx
return mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved

27
stage0/src/Lean/Elab/Tactic/Rewrite.lean generated
View file

@ -42,12 +42,10 @@ def rewriteAll (stx : Syntax) (symm : Bool) (mode : TransparencyMode) : TacticM
let mvarId ← getMainGoal
throwTacticEx `rewrite mvarId "did not find instance of the pattern in the current goal"
def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
let token := stx[0]
let lbrak := stx[1][0]
let rules := stx[1][1].getArgs
let rbrak := stx[1][2]
let loc := expandOptLocation stx[2]
def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
let lbrak := rwRulesSeqStx[0]
let rules := rwRulesSeqStx[1].getArgs
let rbrak := rwRulesSeqStx[2]
-- show initial state up to (incl.) `[`
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let numRules := (rules.size + 1) / 2
@ -60,12 +58,17 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
withRef rule do
let symm := !rule[0].isNone
let term := rule[1]
match loc with
| Location.targets hyps type =>
hyps.forM (rewriteLocalDecl term symm · mode)
if type then
rewriteTarget term symm mode
| Location.wildcard => rewriteAll term symm mode
x symm term
def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
let loc := expandOptLocation stx[2]
withRWRulesSeq stx[0] stx[1] fun symm term => do
match loc with
| Location.targets hyps type =>
hyps.forM (rewriteLocalDecl term symm · mode)
if type then
rewriteTarget term symm mode
| Location.wildcard => rewriteAll term symm mode
@[builtinTactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic :=
evalRewriteCore TransparencyMode.instances

4
stage0/src/Lean/Expr.lean generated
View file

@ -598,6 +598,10 @@ def consumeMData : Expr → Expr
| mdata _ e _ => consumeMData e
| e => e
def mdataExpr! : Expr → Expr
| mdata _ e _ => e
| _ => panic! "mdata expression expected"
def hasLooseBVars (e : Expr) : Bool :=
e.looseBVarRange > 0

599
stage0/stdlib/Init/Conv.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Elab/Tactic/Conv.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.Conv
// Imports: Init Lean.Elab.Tactic.Conv.Basic Lean.Elab.Tactic.Conv.Congr
// Imports: Init Lean.Elab.Tactic.Conv.Basic Lean.Elab.Tactic.Conv.Congr Lean.Elab.Tactic.Conv.Rewrite Lean.Elab.Tactic.Conv.Change
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -16,6 +16,8 @@ extern "C" {
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Basic(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Congr(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Rewrite(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Change(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Tactic_Conv(lean_object* w) {
lean_object * res;
@ -30,6 +32,12 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Conv_Congr(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Conv_Rewrite(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Conv_Change(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

1013
stage0/stdlib/Lean/Elab/Tactic/Conv/Basic.c generated
View file

File diff suppressed because it is too large Load diff

734
stage0/stdlib/Lean/Elab/Tactic/Conv/Change.c generated Normal file
View file

@ -0,0 +1,734 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.Conv.Change
// Imports: Init Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Conv.Basic
#include <lean/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
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__3;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__15;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__5;
lean_object* l_Lean_stringToMessageData(lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__14;
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange(lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__10;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__16;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_changeLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__7;
lean_object* l_Lean_Elab_Tactic_Conv_evalChange(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_filterOldMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__12;
lean_object* l_Lean_Meta_isExprDefEqGuarded(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__1;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__11;
lean_object* l_Lean_Elab_Tactic_Conv_evalChange___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_getLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTacticAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6;
lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__8;
lean_object* l_Lean_Meta_getMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__9;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__4;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__13;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalChange___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_logUnassignedAndAbort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__6;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1___rarg(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalChange___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
x_12 = l_Lean_Elab_Tactic_Conv_changeLhs(x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
return x_12;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Parser");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__2;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Tactic");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__4;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Conv");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__6;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("change");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__8;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid 'change' conv tactic, term");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__11;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("\nis not definitionally equal to current left-hand-side");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__13;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__15;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalChange(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; uint8_t x_12;
x_11 = l_Lean_Elab_Tactic_Conv_evalChange___closed__10;
lean_inc(x_1);
x_12 = l_Lean_Syntax_isOfKind(x_1, x_11);
if (x_12 == 0)
{
lean_object* x_13;
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_13 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1___rarg(x_10);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
lean_dec(x_1);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_16 = l_Lean_Elab_Tactic_Conv_getLhs(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_16) == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = lean_st_ref_get(x_9, x_18);
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = lean_st_ref_get(x_7, x_20);
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_ctor_get(x_24, 1);
lean_inc(x_25);
lean_dec(x_24);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_17);
x_26 = lean_infer_type(x_17, x_6, x_7, x_8, x_9, x_23);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31;
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
x_29 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_29, 0, x_27);
x_30 = 0;
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_31 = l_Lean_Elab_Tactic_elabTermEnsuringType(x_15, x_29, x_30, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_28);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
x_33 = lean_ctor_get(x_31, 1);
lean_inc(x_33);
lean_dec(x_31);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_32);
x_34 = l_Lean_Meta_getMVars(x_32, x_6, x_7, x_8, x_9, x_33);
if (lean_obj_tag(x_34) == 0)
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_35 = lean_ctor_get(x_34, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_dec(x_34);
x_37 = l_Lean_Elab_Tactic_filterOldMVars(x_35, x_25, x_6, x_7, x_8, x_9, x_36);
lean_dec(x_25);
lean_dec(x_35);
x_38 = lean_ctor_get(x_37, 0);
lean_inc(x_38);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
lean_dec(x_37);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
x_40 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_39);
if (lean_obj_tag(x_40) == 0)
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44;
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_17);
lean_inc(x_32);
x_42 = l_Lean_Meta_isExprDefEqGuarded(x_32, x_17, x_6, x_7, x_8, x_9, x_41);
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_unbox(x_43);
lean_dec(x_43);
if (x_44 == 0)
{
lean_object* x_45; 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_53; lean_object* x_54; lean_object* x_55; uint8_t x_56;
x_45 = lean_ctor_get(x_42, 1);
lean_inc(x_45);
lean_dec(x_42);
x_46 = l_Lean_indentExpr(x_32);
x_47 = l_Lean_Elab_Tactic_Conv_evalChange___closed__12;
x_48 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_46);
x_49 = l_Lean_Elab_Tactic_Conv_evalChange___closed__14;
x_50 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
x_51 = l_Lean_indentExpr(x_17);
x_52 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
x_53 = l_Lean_Elab_Tactic_Conv_evalChange___closed__16;
x_54 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
x_55 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTacticAux___spec__2(x_54, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_45);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_56 = !lean_is_exclusive(x_55);
if (x_56 == 0)
{
return x_55;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_57 = lean_ctor_get(x_55, 0);
x_58 = lean_ctor_get(x_55, 1);
lean_inc(x_58);
lean_inc(x_57);
lean_dec(x_55);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
}
}
else
{
lean_object* x_60; lean_object* x_61;
lean_dec(x_17);
x_60 = lean_ctor_get(x_42, 1);
lean_inc(x_60);
lean_dec(x_42);
x_61 = l_Lean_Elab_Tactic_Conv_changeLhs(x_32, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_60);
return x_61;
}
}
else
{
uint8_t x_62;
lean_dec(x_32);
lean_dec(x_17);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_62 = !lean_is_exclusive(x_40);
if (x_62 == 0)
{
return x_40;
}
else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_63 = lean_ctor_get(x_40, 0);
x_64 = lean_ctor_get(x_40, 1);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_40);
x_65 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_65, 0, x_63);
lean_ctor_set(x_65, 1, x_64);
return x_65;
}
}
}
else
{
uint8_t x_66;
lean_dec(x_32);
lean_dec(x_25);
lean_dec(x_17);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_66 = !lean_is_exclusive(x_34);
if (x_66 == 0)
{
return x_34;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_67 = lean_ctor_get(x_34, 0);
x_68 = lean_ctor_get(x_34, 1);
lean_inc(x_68);
lean_inc(x_67);
lean_dec(x_34);
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_67);
lean_ctor_set(x_69, 1, x_68);
return x_69;
}
}
}
else
{
uint8_t x_70;
lean_dec(x_25);
lean_dec(x_17);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_70 = !lean_is_exclusive(x_31);
if (x_70 == 0)
{
return x_31;
}
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_71 = lean_ctor_get(x_31, 0);
x_72 = lean_ctor_get(x_31, 1);
lean_inc(x_72);
lean_inc(x_71);
lean_dec(x_31);
x_73 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
return x_73;
}
}
}
else
{
uint8_t x_74;
lean_dec(x_25);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_74 = !lean_is_exclusive(x_26);
if (x_74 == 0)
{
return x_26;
}
else
{
lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_75 = lean_ctor_get(x_26, 0);
x_76 = lean_ctor_get(x_26, 1);
lean_inc(x_76);
lean_inc(x_75);
lean_dec(x_26);
x_77 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_77, 0, x_75);
lean_ctor_set(x_77, 1, x_76);
return x_77;
}
}
}
else
{
uint8_t x_78;
lean_dec(x_15);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_78 = !lean_is_exclusive(x_16);
if (x_78 == 0)
{
return x_16;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_79 = lean_ctor_get(x_16, 0);
x_80 = lean_ctor_get(x_16, 1);
lean_inc(x_80);
lean_inc(x_79);
lean_dec(x_16);
x_81 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
return x_81;
}
}
}
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalChange___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
x_12 = l_Lean_Elab_Tactic_Conv_evalChange___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_2);
return x_12;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Elab");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Conv_evalChange___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3;
x_2 = l_Lean_Elab_Tactic_Conv_evalChange___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalChange");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalChange), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l_Lean_Elab_Tactic_Conv_evalChange___closed__10;
x_4 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6;
x_5 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_ElabTerm(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Basic(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Tactic_Conv_Change(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_ElabTerm(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Conv_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Tactic_Conv_evalChange___closed__1 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__1);
l_Lean_Elab_Tactic_Conv_evalChange___closed__2 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__2();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__2);
l_Lean_Elab_Tactic_Conv_evalChange___closed__3 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__3();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__3);
l_Lean_Elab_Tactic_Conv_evalChange___closed__4 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__4();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__4);
l_Lean_Elab_Tactic_Conv_evalChange___closed__5 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__5();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__5);
l_Lean_Elab_Tactic_Conv_evalChange___closed__6 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__6();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__6);
l_Lean_Elab_Tactic_Conv_evalChange___closed__7 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__7();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__7);
l_Lean_Elab_Tactic_Conv_evalChange___closed__8 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__8();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__8);
l_Lean_Elab_Tactic_Conv_evalChange___closed__9 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__9();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__9);
l_Lean_Elab_Tactic_Conv_evalChange___closed__10 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__10();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__10);
l_Lean_Elab_Tactic_Conv_evalChange___closed__11 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__11();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__11);
l_Lean_Elab_Tactic_Conv_evalChange___closed__12 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__12();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__12);
l_Lean_Elab_Tactic_Conv_evalChange___closed__13 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__13();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__13);
l_Lean_Elab_Tactic_Conv_evalChange___closed__14 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__14();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__14);
l_Lean_Elab_Tactic_Conv_evalChange___closed__15 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__15();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__15);
l_Lean_Elab_Tactic_Conv_evalChange___closed__16 = _init_l_Lean_Elab_Tactic_Conv_evalChange___closed__16();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalChange___closed__16);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__1);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__2);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__3);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__4);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__5);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__7);
res = l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

704
stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c generated
View file

@ -22,21 +22,28 @@ lean_object* l_Lean_stringToMessageData(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__1;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_List_get___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___closed__3;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__23;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__3;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__17;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__4;
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3;
static lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__5;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isArrow(lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1;
lean_object* l_Lean_Elab_Tactic_Conv_evalLhs_match__1(lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__3;
lean_object* l_Lean_Elab_Tactic_Conv_congr_match__1___rarg(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__21;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__8;
lean_object* l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__2;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isApp(lean_object*);
@ -53,6 +60,7 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_addTrace___at_Lean_Meta_mkCongrLemma___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_congr_match__1(lean_object*);
@ -66,12 +74,16 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___
lean_object* l_Lean_Elab_Tactic_Conv_evalCongr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRhs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_applyRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__15;
extern lean_object* l_Lean_numLitKind;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalArg_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__10;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__18;
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3;
lean_object* l_Lean_Elab_Tactic_Conv_congr_match__2(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__11;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__22;
@ -80,12 +92,14 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__1;
lean_object* l_Lean_Elab_Tactic_Conv_mkConvGoalFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__7;
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___closed__4;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__24;
static lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__2;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__5;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___boxed(lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs___closed__1;
lean_object* l_Lean_Expr_withAppAux___at_Lean_Elab_Tactic_Conv_congr___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_withAppAux___at_Lean_Elab_Tactic_Conv_congr___spec__2___closed__1;
@ -93,6 +107,7 @@ lean_object* lean_array_to_list(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs___closed__2;
static lean_object* l_Lean_Elab_Tactic_Conv_congr___lambda__2___closed__2;
lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_congr_match__2___rarg(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__12;
lean_object* l_Lean_Elab_Tactic_Conv_evalRhs(lean_object*);
@ -100,6 +115,7 @@ size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_congr___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l_Lean_Meta_withMVarContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTacticAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__16;
extern lean_object* l_Lean_Meta_instInhabitedParamInfo;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -112,7 +128,10 @@ lean_object* l_Lean_Elab_Tactic_Conv_evalCongr___boxed(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__20;
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__10;
lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__9;
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___closed__1;
lean_object* l_Lean_Meta_Simp_mkCongrFun(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_withAppAux___at_Lean_Elab_Tactic_Conv_congr___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__4;
@ -131,21 +150,30 @@ lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_obje
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs___closed__3;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__11;
lean_object* lean_mk_array(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__13;
lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Meta_withIncRecDepth___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentD(lean_object*);
lean_object* l_List_lengthTRAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalArg_match__1(lean_object*);
lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs___closed__4;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__14;
lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_congr___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs___closed__3;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___closed__2;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__19;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__8;
static lean_object* l_Lean_Elab_Tactic_Conv_congr___lambda__2___closed__1;
lean_object* l_Lean_Elab_Tactic_Conv_getLhsRhsCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1___rarg(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRhs___boxed(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_Conv_congr___spec__1___closed__9;
@ -2709,6 +2737,657 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalArg_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_apply_2(x_3, x_7, x_8);
return x_9;
}
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalArg_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalArg_match__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_13;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_3);
lean_ctor_set(x_13, 1, x_12);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19;
x_14 = lean_ctor_get(x_2, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_dec(x_2);
x_16 = lean_ctor_get(x_3, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_3, 1);
lean_inc(x_17);
x_18 = lean_ctor_get(x_3, 2);
lean_inc(x_18);
x_19 = lean_nat_dec_lt(x_16, x_17);
if (x_19 == 0)
{
lean_object* x_20;
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_3);
lean_ctor_set(x_20, 1, x_12);
return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_3);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_22 = lean_ctor_get(x_3, 2);
lean_dec(x_22);
x_23 = lean_ctor_get(x_3, 1);
lean_dec(x_23);
x_24 = lean_ctor_get(x_3, 0);
lean_dec(x_24);
x_25 = lean_nat_add(x_16, x_18);
lean_ctor_set(x_3, 0, x_25);
x_26 = lean_nat_dec_eq(x_1, x_16);
lean_dec(x_16);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__5;
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
x_28 = l_Lean_Meta_applyRefl(x_14, x_27, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_28) == 0)
{
lean_object* x_29;
x_29 = lean_ctor_get(x_28, 1);
lean_inc(x_29);
lean_dec(x_28);
x_2 = x_15;
x_12 = x_29;
goto _start;
}
else
{
uint8_t x_31;
lean_dec(x_3);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
x_31 = !lean_is_exclusive(x_28);
if (x_31 == 0)
{
return x_28;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_28, 0);
x_33 = lean_ctor_get(x_28, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_28);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
}
}
}
else
{
lean_dec(x_14);
x_2 = x_15;
goto _start;
}
}
else
{
lean_object* x_36; lean_object* x_37; uint8_t x_38;
lean_dec(x_3);
x_36 = lean_nat_add(x_16, x_18);
x_37 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_17);
lean_ctor_set(x_37, 2, x_18);
x_38 = lean_nat_dec_eq(x_1, x_16);
lean_dec(x_16);
if (x_38 == 0)
{
lean_object* x_39; lean_object* x_40;
x_39 = l_Lean_Elab_Tactic_Conv_evalLhs___rarg___closed__5;
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
x_40 = l_Lean_Meta_applyRefl(x_14, x_39, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_40) == 0)
{
lean_object* x_41;
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
lean_dec(x_40);
x_2 = x_15;
x_3 = x_37;
x_12 = x_41;
goto _start;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
lean_dec(x_37);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
x_43 = lean_ctor_get(x_40, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_40, 1);
lean_inc(x_44);
if (lean_is_exclusive(x_40)) {
lean_ctor_release(x_40, 0);
lean_ctor_release(x_40, 1);
x_45 = x_40;
} else {
lean_dec_ref(x_40);
x_45 = lean_box(0);
}
if (lean_is_scalar(x_45)) {
x_46 = lean_alloc_ctor(1, 2, 0);
} else {
x_46 = x_45;
}
lean_ctor_set(x_46, 0, x_43);
lean_ctor_set(x_46, 1, x_44);
return x_46;
}
}
else
{
lean_dec(x_14);
x_2 = x_15;
x_3 = x_37;
goto _start;
}
}
}
}
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid 'arg' conv tactic, application has only ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" (nondependent) arguments");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(1u);
x_13 = lean_nat_sub(x_1, x_12);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_14 = l_Lean_Elab_Tactic_getMainGoal(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_17 = l_Lean_Elab_Tactic_Conv_congr(x_15, x_7, x_8, x_9, x_10, x_16);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_unsigned_to_nat(0u);
x_21 = l_List_lengthTRAux___rarg(x_18, x_20);
x_22 = lean_nat_dec_lt(x_13, x_21);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_18);
lean_dec(x_13);
x_23 = l_Nat_repr(x_21);
x_24 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_25 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_25, 0, x_24);
x_26 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2;
x_27 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_25);
x_28 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4;
x_29 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_29, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_19);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_30;
}
else
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_31, 0, x_20);
lean_ctor_set(x_31, 1, x_21);
lean_ctor_set(x_31, 2, x_12);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_18);
x_32 = l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1(x_13, x_18, x_31, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_19);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_33 = lean_ctor_get(x_32, 1);
lean_inc(x_33);
lean_dec(x_32);
x_34 = l_List_get___rarg(x_18, x_13, lean_box(0));
lean_dec(x_18);
x_35 = lean_box(0);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
x_37 = l_Lean_Elab_Tactic_replaceMainGoal(x_36, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_33);
return x_37;
}
else
{
uint8_t x_38;
lean_dec(x_18);
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_38 = !lean_is_exclusive(x_32);
if (x_38 == 0)
{
return x_32;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_32, 0);
x_40 = lean_ctor_get(x_32, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_32);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
}
else
{
uint8_t x_42;
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_42 = !lean_is_exclusive(x_17);
if (x_42 == 0)
{
return x_17;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_17, 0);
x_44 = lean_ctor_get(x_17, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_17);
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
}
}
}
else
{
uint8_t x_46;
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_46 = !lean_is_exclusive(x_14);
if (x_46 == 0)
{
return x_14;
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_47 = lean_ctor_get(x_14, 0);
x_48 = lean_ctor_get(x_14, 1);
lean_inc(x_48);
lean_inc(x_47);
lean_dec(x_14);
x_49 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_49, 0, x_47);
lean_ctor_set(x_49, 1, x_48);
return x_49;
}
}
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("invalid 'arg' conv tactic, index must be greater than 0");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Tactic_Conv_evalArg___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("arg");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__7;
x_2 = l_Lean_Elab_Tactic_Conv_evalArg___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_23; uint8_t x_24;
x_23 = l_Lean_Elab_Tactic_Conv_evalArg___closed__4;
lean_inc(x_1);
x_24 = l_Lean_Syntax_isOfKind(x_1, x_23);
if (x_24 == 0)
{
lean_object* x_25;
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_25 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalChoiceAux___spec__1___rarg(x_10);
return x_25;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_26 = lean_unsigned_to_nat(1u);
x_27 = l_Lean_Syntax_getArg(x_1, x_26);
lean_dec(x_1);
x_28 = l_Lean_numLitKind;
x_29 = l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(x_28, x_27);
lean_dec(x_27);
if (lean_obj_tag(x_29) == 0)
{
lean_object* x_30;
x_30 = lean_unsigned_to_nat(0u);
x_11 = x_30;
goto block_22;
}
else
{
lean_object* x_31;
x_31 = lean_ctor_get(x_29, 0);
lean_inc(x_31);
lean_dec(x_29);
x_11 = x_31;
goto block_22;
}
}
block_22:
{
lean_object* x_12; uint8_t x_13;
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_nat_dec_eq(x_11, x_12);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_box(0);
x_15 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1(x_11, x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_11);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; uint8_t x_18;
lean_dec(x_11);
x_16 = l_Lean_Elab_Tactic_Conv_evalArg___closed__2;
x_17 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTacticAux___spec__2(x_16, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
return x_17;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_17, 0);
x_20 = lean_ctor_get(x_17, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_17);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
}
}
lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
lean_object* x_13;
x_13 = l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_evalArg___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
return x_13;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
x_12 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_2);
lean_dec(x_1);
return x_12;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalArg");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalCongr___closed__13;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalArg), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l_Lean_Elab_Tactic_Conv_evalArg___closed__4;
x_4 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2;
x_5 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_Main(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Basic(lean_object*);
@ -2859,6 +3538,31 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs___closed__5);
res = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1 = _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__1);
l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2 = _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__2);
l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3 = _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__3);
l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4 = _init_l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___lambda__1___closed__4);
l_Lean_Elab_Tactic_Conv_evalArg___closed__1 = _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___closed__1);
l_Lean_Elab_Tactic_Conv_evalArg___closed__2 = _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__2();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___closed__2);
l_Lean_Elab_Tactic_Conv_evalArg___closed__3 = _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__3();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___closed__3);
l_Lean_Elab_Tactic_Conv_evalArg___closed__4 = _init_l_Lean_Elab_Tactic_Conv_evalArg___closed__4();
lean_mark_persistent(l_Lean_Elab_Tactic_Conv_evalArg___closed__4);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__1);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__2);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg___closed__3);
res = l___regBuiltin_Lean_Elab_Tactic_Conv_evalArg(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

747
stage0/stdlib/Lean/Elab/Tactic/Conv/Rewrite.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.Conv.Rewrite
// Imports: Init
// Imports: Init Lean.Meta.Tactic.Rewrite Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Conv.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -13,7 +13,693 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Elab_Tactic_withRWRulesSeq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalERewrite___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12;
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_withMainContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13;
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17;
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10;
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_rewrite(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalERewrite(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5;
lean_object* l_Lean_Elab_Tactic_Conv_getLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_withSynthesizeImp___rarg(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16;
lean_object* l_Lean_Elab_Tactic_Conv_updateLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewrite___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewrite(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11;
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1(lean_object* x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
uint8_t x_14; lean_object* x_15;
x_14 = 1;
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_15 = l_Lean_Elab_Tactic_elabTerm(x_1, x_2, x_14, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_18 = l_Lean_Elab_Tactic_getMainGoal(x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_17);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_21 = l_Lean_Elab_Tactic_Conv_getLhs(x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_20);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = lean_box(0);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
x_25 = l_Lean_Meta_rewrite(x_19, x_22, x_16, x_3, x_24, x_4, x_9, x_10, x_11, x_12, x_23);
if (lean_obj_tag(x_25) == 0)
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
lean_dec(x_25);
x_28 = lean_ctor_get(x_26, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_30 = l_Lean_Elab_Tactic_Conv_updateLhs(x_28, x_29, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_27);
if (lean_obj_tag(x_30) == 0)
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_ctor_get(x_30, 1);
lean_inc(x_31);
lean_dec(x_30);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_32 = l_Lean_Elab_Tactic_getMainGoal(x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_31);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_33 = lean_ctor_get(x_32, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_inc(x_34);
lean_dec(x_32);
x_35 = lean_ctor_get(x_26, 2);
lean_inc(x_35);
lean_dec(x_26);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_33);
lean_ctor_set(x_36, 1, x_35);
x_37 = l_Lean_Elab_Tactic_replaceMainGoal(x_36, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_34);
return x_37;
}
else
{
uint8_t x_38;
lean_dec(x_26);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_38 = !lean_is_exclusive(x_32);
if (x_38 == 0)
{
return x_32;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_32, 0);
x_40 = lean_ctor_get(x_32, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_32);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
else
{
uint8_t x_42;
lean_dec(x_26);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_42 = !lean_is_exclusive(x_30);
if (x_42 == 0)
{
return x_30;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_30, 0);
x_44 = lean_ctor_get(x_30, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_30);
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
}
}
}
else
{
uint8_t x_46;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_46 = !lean_is_exclusive(x_25);
if (x_46 == 0)
{
return x_25;
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_47 = lean_ctor_get(x_25, 0);
x_48 = lean_ctor_get(x_25, 1);
lean_inc(x_48);
lean_inc(x_47);
lean_dec(x_25);
x_49 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_49, 0, x_47);
lean_ctor_set(x_49, 1, x_48);
return x_49;
}
}
}
else
{
uint8_t x_50;
lean_dec(x_19);
lean_dec(x_16);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_50 = !lean_is_exclusive(x_21);
if (x_50 == 0)
{
return x_21;
}
else
{
lean_object* x_51; lean_object* x_52; lean_object* x_53;
x_51 = lean_ctor_get(x_21, 0);
x_52 = lean_ctor_get(x_21, 1);
lean_inc(x_52);
lean_inc(x_51);
lean_dec(x_21);
x_53 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_53, 0, x_51);
lean_ctor_set(x_53, 1, x_52);
return x_53;
}
}
}
else
{
uint8_t x_54;
lean_dec(x_16);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_54 = !lean_is_exclusive(x_18);
if (x_54 == 0)
{
return x_18;
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57;
x_55 = lean_ctor_get(x_18, 0);
x_56 = lean_ctor_get(x_18, 1);
lean_inc(x_56);
lean_inc(x_55);
lean_dec(x_18);
x_57 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
return x_57;
}
}
}
else
{
uint8_t x_58;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_58 = !lean_is_exclusive(x_15);
if (x_58 == 0)
{
return x_15;
}
else
{
lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_59 = lean_ctor_get(x_15, 0);
x_60 = lean_ctor_get(x_15, 1);
lean_inc(x_60);
lean_inc(x_59);
lean_dec(x_15);
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_59);
lean_ctor_set(x_61, 1, x_60);
return x_61;
}
}
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_19; lean_object* x_20;
x_13 = lean_box(0);
x_14 = lean_box(x_2);
x_15 = lean_box(x_1);
x_16 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1___boxed), 13, 4);
lean_closure_set(x_16, 0, x_3);
lean_closure_set(x_16, 1, x_13);
lean_closure_set(x_16, 2, x_14);
lean_closure_set(x_16, 3, x_15);
x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withMainContext___rarg), 10, 3);
lean_closure_set(x_17, 0, x_16);
lean_closure_set(x_17, 1, x_4);
lean_closure_set(x_17, 2, x_5);
x_18 = 0;
x_19 = 1;
x_20 = l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_withSynthesizeImp___rarg(x_17, x_18, x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_20;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_12 = lean_unsigned_to_nat(0u);
x_13 = l_Lean_Syntax_getArg(x_2, x_12);
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_2, x_14);
x_16 = lean_box(x_1);
x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2___boxed), 12, 1);
lean_closure_set(x_17, 0, x_16);
x_18 = l_Lean_Elab_Tactic_withRWRulesSeq(x_13, x_15, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_15);
return x_18;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
uint8_t x_14; uint8_t x_15; lean_object* x_16;
x_14 = lean_unbox(x_3);
lean_dec(x_3);
x_15 = lean_unbox(x_4);
lean_dec(x_4);
x_16 = l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__1(x_1, x_2, x_14, x_15, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
return x_16;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
_start:
{
uint8_t x_13; uint8_t x_14; lean_object* x_15;
x_13 = lean_unbox(x_1);
lean_dec(x_1);
x_14 = lean_unbox(x_2);
lean_dec(x_2);
x_15 = l_Lean_Elab_Tactic_Conv_evalRewriteCore___lambda__2(x_13, x_14, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_15;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewriteCore___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
uint8_t x_12; lean_object* x_13;
x_12 = lean_unbox(x_1);
lean_dec(x_1);
x_13 = l_Lean_Elab_Tactic_Conv_evalRewriteCore(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_2);
return x_13;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewrite(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
uint8_t x_11; lean_object* x_12;
x_11 = 3;
x_12 = l_Lean_Elab_Tactic_Conv_evalRewriteCore(x_11, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_12;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalRewrite___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_Conv_evalRewrite(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Parser");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Tactic");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Conv");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("rewrite");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Elab");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalRewrite");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalRewrite___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10;
x_4 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16;
x_5 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalERewrite(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
uint8_t x_11; lean_object* x_12;
x_11 = 1;
x_12 = l_Lean_Elab_Tactic_Conv_evalRewriteCore(x_11, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_12;
}
}
lean_object* l_Lean_Elab_Tactic_Conv_evalERewrite___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_Conv_evalERewrite(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("erewrite");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("evalERewrite");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14;
x_2 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Conv_evalERewrite___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4;
x_5 = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Rewrite(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Rewrite(lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Conv_Basic(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Tactic_Conv_Rewrite(lean_object* w) {
lean_object * res;
@ -22,6 +708,65 @@ _G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Rewrite(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Rewrite(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Conv_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__1);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__2);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__3);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__4);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__5);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__6);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__7);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__8);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__9);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__10);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__11);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__12);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__13);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__14);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__15);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__16);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite___closed__17);
res = l___regBuiltin_Lean_Elab_Tactic_Conv_evalRewrite(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__1);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__2);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__3);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__4);
l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite___closed__5);
res = l___regBuiltin_Lean_Elab_Tactic_Conv_evalERewrite(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

114
stage0/stdlib/Lean/Elab/Tactic/ElabTerm.c generated
View file

@ -40,7 +40,6 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExact(lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalNativeDecide(lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermForApply_match__1(lean_object*);
lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_withoutModifyingStateWithInfoAndMessagesImpl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalWithReducible(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithReducible___closed__3;
@ -59,12 +58,10 @@ lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType_match__1___rarg(lean_object
lean_object* l_Lean_Elab_Tactic_closeMainGoalUsing(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine___closed__3;
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_elabTermForApply___closed__1;
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_preprocessPropToDecide___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalDecide___boxed(lean_object*);
lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRename(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalConstructor___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDecide___closed__1;
@ -80,6 +77,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles__
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine___closed__2;
lean_object* l_Lean_Elab_Tactic_evalNativeDecide___boxed(lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar_match__3(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalRename___lambda__1___closed__1;
lean_object* l_Lean_Elab_Tactic_evalApply(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -107,12 +105,11 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalConstructor___closed__5;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExistsIntro(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExact___closed__4;
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_apply(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_findSomeRevM_x3f_find___at_Lean_Elab_Tactic_evalRename___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExistsIntro___closed__3;
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_filterOldMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRename___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_intro1Core(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalNativeDecide___rarg___lambda__1___closed__7;
@ -143,13 +140,13 @@ static lean_object* l_Lean_Elab_Tactic_evalExact___closed__8;
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithReducibleAndInstances___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithReducible(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_abortTacticExceptionId;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithReducible___closed__1;
lean_object* l_Lean_Elab_Tactic_getMainTarget(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalExact___closed__1;
static lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___lambda__1___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithReducibleAndInstances___closed__1;
lean_object* l_Lean_Elab_Tactic_logUnassignedAndAbort___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermForApply___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermForApply___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -161,14 +158,15 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRename(lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExact___closed__3;
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalRefine___closed__3;
lean_object* l_Std_PersistentArray_findSomeRevMAux___at_Lean_Elab_Tactic_evalRename___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRename___closed__1;
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_resolveId_x3f(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalRefine_x27___closed__1;
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getLocalInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar_match__1(lean_object*);
@ -199,21 +197,21 @@ static lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_pr
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalNativeDecide___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_assignExprMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalRefine___closed__1;
static lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1;
lean_object* l_Lean_Meta_getMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_filterOldMVars___closed__1;
lean_object* l_Lean_Elab_Tactic_evalExistsIntro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalExact___closed__1;
lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalApply___closed__3;
static lean_object* l_Lean_Elab_Tactic_evalNativeDecide___rarg___lambda__1___closed__4;
static lean_object* l_Lean_Elab_Tactic_evalRefine___closed__2;
static lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___lambda__1___closed__7;
lean_object* l_Lean_Elab_Tactic_evalWithReducible___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
lean_object* l_Lean_Elab_Tactic_refineCore_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_preprocessPropToDecide(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabAsFVar_match__2(lean_object*);
@ -232,6 +230,7 @@ lean_object* l_Lean_Elab_Tactic_refineCore___lambda__1___boxed(lean_object*, lea
static lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_preprocessPropToDecide___lambda__2___closed__1;
lean_object* l_Lean_Elab_Tactic_elabAsFVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalApply___closed__2;
lean_object* l_Lean_Elab_Tactic_evalDecide(lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalExact___closed__5;
@ -245,6 +244,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalNativeDecide___closed__5
static lean_object* l_Lean_Elab_Tactic_evalApply___closed__2;
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalConstructor___closed__2;
lean_object* l_Lean_Elab_Tactic_filterOldMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalApply(lean_object*);
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalWithReducibleAndInstances___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -280,6 +280,7 @@ static lean_object* l_Lean_Elab_Tactic_evalRename___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermWithHoles___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_logUnassignedAndAbort(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalNativeDecide___closed__1;
static lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___closed__1;
@ -303,7 +304,6 @@ lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType___boxed(lean_object*, lean_
lean_object* l_Lean_Elab_Tactic_elabTermWithHoles___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalApply___closed__3;
lean_object* l_Lean_Meta_withNewMCtxDepth___at_Lean_Elab_Tactic_evalRename___spec__7(lean_object*);
static lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalDecide___rarg___lambda__1___closed__1;
@ -1161,7 +1161,7 @@ x_13 = l_Lean_Elab_Tactic_closeMainGoalUsing(x_1, x_12, x_3, x_4, x_5, x_6, x_7,
return x_13;
}
}
static lean_object* _init_l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1() {
static lean_object* _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -1173,26 +1173,26 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(lean_object* x_1) {
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1;
x_2 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1;
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_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg), 1, 0);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg), 1, 0);
return x_9;
}
}
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Elab_Tactic_logUnassignedAndAbort(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
@ -1237,7 +1237,7 @@ lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_12, 1);
lean_inc(x_21);
lean_dec(x_12);
x_22 = l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(x_21);
x_22 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg(x_21);
return x_22;
}
}
@ -1265,11 +1265,11 @@ return x_26;
}
}
}
lean_object* l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
x_9 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
@ -1281,17 +1281,17 @@ lean_dec(x_1);
return x_9;
}
}
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Elab_Tactic_logUnassignedAndAbort___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_3);
lean_dec(x_2);
return x_11;
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, size_t x_4, size_t x_5, lean_object* x_6) {
_start:
{
uint8_t x_7;
@ -1332,7 +1332,7 @@ return x_6;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1() {
static lean_object* _init_l_Lean_Elab_Tactic_filterOldMVars___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -1341,7 +1341,7 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Lean_Elab_Tactic_filterOldMVars(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
@ -1366,7 +1366,7 @@ if (x_16 == 0)
lean_object* x_17;
lean_dec(x_14);
lean_dec(x_13);
x_17 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_17 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
lean_ctor_set(x_10, 0, x_17);
return x_10;
}
@ -1379,7 +1379,7 @@ if (x_18 == 0)
lean_object* x_19;
lean_dec(x_14);
lean_dec(x_13);
x_19 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_19 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
lean_ctor_set(x_10, 0, x_19);
return x_10;
}
@ -1389,8 +1389,8 @@ size_t x_20; size_t x_21; lean_object* x_22; lean_object* x_23;
x_20 = 0;
x_21 = lean_usize_of_nat(x_14);
lean_dec(x_14);
x_22 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_23 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1(x_2, x_13, x_1, x_20, x_21, x_22);
x_22 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_23 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1(x_2, x_13, x_1, x_20, x_21, x_22);
lean_ctor_set(x_10, 0, x_23);
return x_10;
}
@ -1415,7 +1415,7 @@ if (x_29 == 0)
lean_object* x_30; lean_object* x_31;
lean_dec(x_27);
lean_dec(x_26);
x_30 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_30 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_25);
@ -1430,7 +1430,7 @@ if (x_32 == 0)
lean_object* x_33; lean_object* x_34;
lean_dec(x_27);
lean_dec(x_26);
x_33 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_33 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_25);
@ -1442,8 +1442,8 @@ size_t x_35; size_t x_36; lean_object* x_37; lean_object* x_38; lean_object* x_3
x_35 = 0;
x_36 = lean_usize_of_nat(x_27);
lean_dec(x_27);
x_37 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_38 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1(x_2, x_26, x_1, x_35, x_36, x_37);
x_37 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_38 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1(x_2, x_26, x_1, x_35, x_36, x_37);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_25);
@ -1453,7 +1453,7 @@ return x_39;
}
}
}
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
@ -1461,17 +1461,17 @@ x_7 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_8 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_9 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___spec__1(x_1, x_2, x_3, x_7, x_8, x_6);
x_9 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_filterOldMVars___spec__1(x_1, x_2, x_3, x_7, x_8, x_6);
lean_dec(x_3);
lean_dec(x_1);
return x_9;
}
}
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
lean_object* l_Lean_Elab_Tactic_filterOldMVars___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
x_8 = l_Lean_Elab_Tactic_filterOldMVars(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
@ -1564,7 +1564,7 @@ lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(x_25, x_18, x_7, x_8, x_9, x_10, x_26);
x_27 = l_Lean_Elab_Tactic_filterOldMVars(x_25, x_18, x_7, x_8, x_9, x_10, x_26);
lean_dec(x_18);
lean_dec(x_25);
x_28 = lean_ctor_get(x_27, 0);
@ -1572,7 +1572,7 @@ lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(x_28, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_29);
x_30 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_28, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_29);
if (lean_obj_tag(x_30) == 0)
{
uint8_t x_31;
@ -2203,7 +2203,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_elabTermWithHoles___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_1 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_2 = lean_array_to_list(lean_box(0), x_1);
return x_2;
}
@ -2266,7 +2266,7 @@ if (x_30 == 0)
lean_object* x_98;
lean_dec(x_28);
lean_dec(x_26);
x_98 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_98 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_31 = x_98;
x_32 = x_27;
goto block_97;
@ -2280,7 +2280,7 @@ if (x_99 == 0)
lean_object* x_100;
lean_dec(x_28);
lean_dec(x_26);
x_100 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_100 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_31 = x_100;
x_32 = x_27;
goto block_97;
@ -2291,7 +2291,7 @@ size_t x_101; size_t x_102; lean_object* x_103; lean_object* x_104; lean_object*
x_101 = 0;
x_102 = lean_usize_of_nat(x_28);
lean_dec(x_28);
x_103 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_103 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -2320,7 +2320,7 @@ x_34 = lean_nat_dec_lt(x_29, x_33);
if (x_34 == 0)
{
lean_object* x_82;
x_82 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_82 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_35 = x_82;
x_36 = x_32;
goto block_81;
@ -2332,7 +2332,7 @@ x_83 = lean_nat_dec_le(x_33, x_33);
if (x_83 == 0)
{
lean_object* x_84;
x_84 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_84 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_35 = x_84;
x_36 = x_32;
goto block_81;
@ -2342,7 +2342,7 @@ else
size_t x_85; size_t x_86; lean_object* x_87; lean_object* x_88;
x_85 = 0;
x_86 = lean_usize_of_nat(x_33);
x_87 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_87 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_88 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__2(x_31, x_85, x_86, x_87, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_32);
if (lean_obj_tag(x_88) == 0)
{
@ -2400,7 +2400,7 @@ if (x_34 == 0)
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
lean_dec(x_33);
lean_dec(x_31);
x_37 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_36);
x_37 = l_Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_36);
lean_dec(x_20);
lean_dec(x_35);
x_38 = lean_ctor_get(x_37, 0);
@ -2414,7 +2414,7 @@ lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_40 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(x_38, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_39);
x_40 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_38, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_39);
if (lean_obj_tag(x_40) == 0)
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
@ -2467,7 +2467,7 @@ if (x_48 == 0)
lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
lean_dec(x_33);
lean_dec(x_31);
x_49 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_36);
x_49 = l_Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_36);
lean_dec(x_20);
lean_dec(x_35);
x_50 = lean_ctor_get(x_49, 0);
@ -2481,7 +2481,7 @@ lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_52 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(x_50, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_51);
x_52 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_50, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_51);
if (lean_obj_tag(x_52) == 0)
{
lean_object* x_53; lean_object* x_54; lean_object* x_55;
@ -2531,7 +2531,7 @@ size_t x_60; size_t x_61; lean_object* x_62; lean_object* x_63;
x_60 = 0;
x_61 = lean_usize_of_nat(x_33);
lean_dec(x_33);
x_62 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1;
x_62 = l_Lean_Elab_Tactic_filterOldMVars___closed__1;
x_63 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabTermWithHoles___spec__1(x_31, x_60, x_61, x_62, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_36);
lean_dec(x_31);
if (lean_obj_tag(x_63) == 0)
@ -2542,7 +2542,7 @@ lean_inc(x_64);
x_65 = lean_ctor_get(x_63, 1);
lean_inc(x_65);
lean_dec(x_63);
x_66 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_65);
x_66 = l_Lean_Elab_Tactic_filterOldMVars(x_35, x_20, x_9, x_10, x_11, x_12, x_65);
lean_dec(x_20);
lean_dec(x_35);
x_67 = lean_ctor_get(x_66, 0);
@ -2556,7 +2556,7 @@ lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
x_69 = l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort(x_67, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_68);
x_69 = l_Lean_Elab_Tactic_logUnassignedAndAbort(x_67, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_68);
if (lean_obj_tag(x_69) == 0)
{
lean_object* x_70; lean_object* x_71; lean_object* x_72;
@ -8432,10 +8432,10 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_SyntheticMVars(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1 = _init_l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1);
l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1 = _init_l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_filterOldMVars___closed__1);
l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1 = _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___rarg___closed__1);
l_Lean_Elab_Tactic_filterOldMVars___closed__1 = _init_l_Lean_Elab_Tactic_filterOldMVars___closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_filterOldMVars___closed__1);
l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalExact___spec__1___rarg___closed__1 = _init_l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalExact___spec__1___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalExact___spec__1___rarg___closed__1);
l_Lean_Elab_Tactic_evalExact___closed__1 = _init_l_Lean_Elab_Tactic_evalExact___closed__1();

1466
stage0/stdlib/Lean/Elab/Tactic/Rewrite.c generated
View file

File diff suppressed because it is too large Load diff

89
stage0/stdlib/Lean/Expr.c generated
View file

@ -224,6 +224,7 @@ lean_object* l_Lean_Expr_getRevArgD_match__1(lean_object*);
lean_object* l_Lean_Expr_replaceFVars(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_361____closed__25;
lean_object* l_Lean_Expr_mdataExpr_x21(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_361____closed__28;
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Expr_letName_x21___boxed(lean_object*);
@ -416,6 +417,7 @@ lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98
static lean_object* l_Lean_Expr_isCharLit___closed__3;
static lean_object* l_Lean_mkEM___closed__5;
static lean_object* l_Lean_mkOr___closed__2;
static lean_object* l_Lean_Expr_mdataExpr_x21___closed__3;
static lean_object* l_Lean_Literal_type___closed__4;
static lean_object* l_Lean_mkDecIsTrue___closed__4;
lean_object* lean_expr_mk_lit(lean_object*);
@ -690,6 +692,7 @@ lean_object* l_Lean_ExprStructEq_hash_match__1___rarg(lean_object*, lean_object*
uint8_t l_Lean_Expr_binderInfo(lean_object*);
uint64_t lean_uint64_mix_hash(uint64_t, uint64_t);
uint8_t l_Lean_Expr_isOptParam(lean_object*);
lean_object* l_Lean_Expr_mdataExpr_x21___boxed(lean_object*);
lean_object* l_Lean_instHashableLiteral;
uint8_t l_Lean_Expr_isAtomic(lean_object*);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
@ -763,6 +766,7 @@ uint64_t l_Lean_BinderInfo_hash(uint8_t);
static lean_object* l_Lean_Expr_setPPUniverses___closed__2;
lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParamsArray___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_mdataExpr_x21___closed__2;
lean_object* l_Lean_mkApp10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_mkNot___closed__3;
lean_object* l_Lean_Expr_isApp___boxed(lean_object*);
@ -796,6 +800,7 @@ lean_object* l_Lean_Expr_hasAnyFVar_visit(lean_object*, lean_object*);
lean_object* lean_expr_update_const(lean_object*, lean_object*);
static lean_object* l_Lean_Expr_updateSort_x21___closed__1;
lean_object* l_Lean_Expr_isConst___boxed(lean_object*);
static lean_object* l_Lean_Expr_mdataExpr_x21___closed__1;
lean_object* l_Lean_Expr_isConstOf_match__1(lean_object*);
uint64_t lean_string_hash(lean_object*);
lean_object* l_Lean_Expr_isNatLit___boxed(lean_object*);
@ -9915,6 +9920,64 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Expr_mdataExpr_x21___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Expr.mdataExpr!");
return x_1;
}
}
static lean_object* _init_l_Lean_Expr_mdataExpr_x21___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mdata expression expected");
return x_1;
}
}
static lean_object* _init_l_Lean_Expr_mdataExpr_x21___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_mdataExpr_x21___closed__1;
x_3 = lean_unsigned_to_nat(603u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_mdataExpr_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
lean_object* l_Lean_Expr_mdataExpr_x21(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 10)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = l_Lean_instInhabitedExpr;
x_4 = l_Lean_Expr_mdataExpr_x21___closed__3;
x_5 = lean_panic_fn(x_3, x_4);
return x_5;
}
}
}
lean_object* l_Lean_Expr_mdataExpr_x21___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Expr_mdataExpr_x21(x_1);
lean_dec(x_1);
return x_2;
}
}
uint8_t l_Lean_Expr_hasLooseBVars(lean_object* x_1) {
_start:
{
@ -12259,7 +12322,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateApp_x21___closed__1;
x_3 = lean_unsigned_to_nat(867u);
x_3 = lean_unsigned_to_nat(871u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12331,7 +12394,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateConst_x21___closed__1;
x_3 = lean_unsigned_to_nat(876u);
x_3 = lean_unsigned_to_nat(880u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12410,7 +12473,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateSort_x21___closed__1;
x_3 = lean_unsigned_to_nat(885u);
x_3 = lean_unsigned_to_nat(889u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_updateSort_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12494,7 +12557,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateMData_x21___closed__1;
x_3 = lean_unsigned_to_nat(902u);
x_3 = lean_unsigned_to_nat(906u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateMData_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12565,7 +12628,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateProj_x21___closed__1;
x_3 = lean_unsigned_to_nat(907u);
x_3 = lean_unsigned_to_nat(911u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_updateProj_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12649,7 +12712,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateForall_x21___closed__1;
x_3 = lean_unsigned_to_nat(916u);
x_3 = lean_unsigned_to_nat(920u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12726,7 +12789,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateForallE_x21___closed__1;
x_3 = lean_unsigned_to_nat(921u);
x_3 = lean_unsigned_to_nat(925u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12814,7 +12877,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLambda_x21___closed__1;
x_3 = lean_unsigned_to_nat(930u);
x_3 = lean_unsigned_to_nat(934u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12891,7 +12954,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1;
x_3 = lean_unsigned_to_nat(935u);
x_3 = lean_unsigned_to_nat(939u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12969,7 +13032,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLet_x21___closed__1;
x_3 = lean_unsigned_to_nat(944u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -16871,6 +16934,12 @@ l_Lean_Expr_letName_x21___closed__2 = _init_l_Lean_Expr_letName_x21___closed__2(
lean_mark_persistent(l_Lean_Expr_letName_x21___closed__2);
l_Lean_Expr_letName_x21___closed__3 = _init_l_Lean_Expr_letName_x21___closed__3();
lean_mark_persistent(l_Lean_Expr_letName_x21___closed__3);
l_Lean_Expr_mdataExpr_x21___closed__1 = _init_l_Lean_Expr_mdataExpr_x21___closed__1();
lean_mark_persistent(l_Lean_Expr_mdataExpr_x21___closed__1);
l_Lean_Expr_mdataExpr_x21___closed__2 = _init_l_Lean_Expr_mdataExpr_x21___closed__2();
lean_mark_persistent(l_Lean_Expr_mdataExpr_x21___closed__2);
l_Lean_Expr_mdataExpr_x21___closed__3 = _init_l_Lean_Expr_mdataExpr_x21___closed__3();
lean_mark_persistent(l_Lean_Expr_mdataExpr_x21___closed__3);
l_Lean_Expr_replaceFVar___closed__1 = _init_l_Lean_Expr_replaceFVar___closed__1();
lean_mark_persistent(l_Lean_Expr_replaceFVar___closed__1);
l_Lean_Expr_instToStringExpr___closed__1 = _init_l_Lean_Expr_instToStringExpr___closed__1();

12
stage0/stdlib/Lean/Meta/Closure.c generated
View file

@ -4154,7 +4154,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__2;
x_3 = lean_unsigned_to_nat(902u);
x_3 = lean_unsigned_to_nat(906u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4183,7 +4183,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__5;
x_3 = lean_unsigned_to_nat(907u);
x_3 = lean_unsigned_to_nat(911u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4212,7 +4212,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__8;
x_3 = lean_unsigned_to_nat(867u);
x_3 = lean_unsigned_to_nat(871u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4241,7 +4241,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__11;
x_3 = lean_unsigned_to_nat(935u);
x_3 = lean_unsigned_to_nat(939u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4270,7 +4270,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__14;
x_3 = lean_unsigned_to_nat(921u);
x_3 = lean_unsigned_to_nat(925u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4299,7 +4299,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__17;
x_3 = lean_unsigned_to_nat(944u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__18;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

@ -14778,7 +14778,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__2;
x_3 = lean_unsigned_to_nat(902u);
x_3 = lean_unsigned_to_nat(906u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14807,7 +14807,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__5;
x_3 = lean_unsigned_to_nat(907u);
x_3 = lean_unsigned_to_nat(911u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14836,7 +14836,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__8;
x_3 = lean_unsigned_to_nat(935u);
x_3 = lean_unsigned_to_nat(939u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14865,7 +14865,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__11;
x_3 = lean_unsigned_to_nat(921u);
x_3 = lean_unsigned_to_nat(925u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14894,7 +14894,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__14;
x_3 = lean_unsigned_to_nat(944u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c generated
View file

@ -11126,7 +11126,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_SimpLemma_getValue___closed__1;
x_2 = l_Lean_Meta_SimpLemma_getValue___closed__2;
x_3 = lean_unsigned_to_nat(876u);
x_3 = lean_unsigned_to_nat(880u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_SimpLemma_getValue___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/Transform.c generated
View file

@ -870,7 +870,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__2;
x_3 = lean_unsigned_to_nat(935u);
x_3 = lean_unsigned_to_nat(939u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -977,7 +977,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__1;
x_3 = lean_unsigned_to_nat(921u);
x_3 = lean_unsigned_to_nat(925u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1084,7 +1084,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__1;
x_3 = lean_unsigned_to_nat(944u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1222,7 +1222,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__1;
x_3 = lean_unsigned_to_nat(902u);
x_3 = lean_unsigned_to_nat(906u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1296,7 +1296,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__1;
x_3 = lean_unsigned_to_nat(907u);
x_3 = lean_unsigned_to_nat(911u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

14
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -11543,7 +11543,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__2;
x_3 = lean_unsigned_to_nat(885u);
x_3 = lean_unsigned_to_nat(889u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11626,7 +11626,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__1;
x_3 = lean_unsigned_to_nat(876u);
x_3 = lean_unsigned_to_nat(880u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11712,7 +11712,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__1;
x_3 = lean_unsigned_to_nat(935u);
x_3 = lean_unsigned_to_nat(939u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11819,7 +11819,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__1;
x_3 = lean_unsigned_to_nat(921u);
x_3 = lean_unsigned_to_nat(925u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11926,7 +11926,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__1;
x_3 = lean_unsigned_to_nat(944u);
x_3 = lean_unsigned_to_nat(948u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12060,7 +12060,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__1;
x_3 = lean_unsigned_to_nat(902u);
x_3 = lean_unsigned_to_nat(906u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12146,7 +12146,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__1;
x_3 = lean_unsigned_to_nat(907u);
x_3 = lean_unsigned_to_nat(911u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);