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 2020-11-02 13:32:03 -08:00
parent f64bd9e1e3
commit 876345bfa6
15 changed files with 1218 additions and 1118 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
stage0/src/Init/Core.lean generated
View file

@ -92,12 +92,10 @@ def Not (a : Prop) : Prop := a → False
inductive Eq {α : Sort u} (a : α) : α → Prop
| refl {} : Eq a a
@[elabAsEliminator, inline, reducible]
def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
Eq.rec (motive := fun α _ => motive α) m h
@[elabAsEliminator, inline, reducible]
def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : Eq a b) (m : motive a) : motive b :=
Eq.ndrec m h
/-
@ -142,7 +140,6 @@ structure Iff (a b : Prop) : Prop :=
@[matchPattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
@[elabAsEliminator]
theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
Eq.ndrec h₂ h₁
@ -456,7 +453,7 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf
/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i
@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i
/- Boolean operators -/
@ -520,7 +517,6 @@ theorem id.def {α : Sort u} (a : α) : id a = a := rfl
@[macroInline] def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α :=
h ▸ b
@[elabAsEliminator]
theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
h₁ ▸ h₂
@ -601,11 +597,9 @@ theorem neTrueOfEqFalse : ∀ {b : Bool}, b = false → b ≠ true
section
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@[elabAsEliminator]
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
@HEq.rec α a (fun b _ => motive b) m β b h
@[elabAsEliminator]
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : motive a) : motive b :=
@HEq.rec α a (fun b _ => motive b) m β b h
@ -1130,14 +1124,12 @@ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
| base : ∀ a b, r a b → TC r a b
| trans : ∀ a b c, TC r a b → TC r b c → TC r a c
@[elabAsEliminator]
theorem TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
(m₁ : ∀ (a b : α), r a b → C a b)
(m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
{a b : α} (h : TC r a b) : C a b :=
@TC.rec α r (fun a b _ => C a b) m₁ m₂ a b h
@[elabAsEliminator]
theorem TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
{a b : α} (h : TC r a b)
(m₁ : ∀ (a b : α), r a b → C a b)
@ -1341,8 +1333,6 @@ theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a)
namespace Quot
axiom sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
attribute [elabAsEliminator] lift ind
protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v}
(f : α → β)
(c : (a b : α) → r a b → f a = f b)
@ -1356,11 +1346,9 @@ protected theorem indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot
: (ind p (Quot.mk r a) : motive (Quot.mk r a)) = p a :=
rfl
@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
protected abbrev liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : (a b : α) → r a b → f a = f b) : β :=
lift f c q
@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop}
(q : Quot r)
(h : (a : α) → motive (Quot.mk r a))
@ -1393,23 +1381,20 @@ protected theorem liftIndepPr1
induction q using Quot.ind
exact rfl
@[reducible, elabAsEliminator, inline]
protected def rec
protected abbrev rec
(f : (a : α) → motive (Quot.mk r a))
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
(q : Quot r) : motive q :=
Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
@[reducible, elabAsEliminator, inline]
protected def recOn
protected abbrev recOn
(q : Quot r)
(f : (a : α) → motive (Quot.mk r a))
(h : (a b : α) → (p : r a b) → Eq.ndrec (f a) (sound p) = f b)
: motive q :=
Quot.rec f h q
@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton
protected abbrev recOnSubsingleton
[h : (a : α) → Subsingleton (motive (Quot.mk r a))]
(q : Quot r)
(f : (a : α) → motive (Quot.mk r a))
@ -1418,8 +1403,7 @@ protected def recOnSubsingleton
apply f
apply Subsingleton.elim
@[reducible, elabAsEliminator, inline]
protected def hrecOn
protected abbrev hrecOn
(q : Quot r)
(f : (a : α) → motive (Quot.mk r a))
(c : (a b : α) → (p : r a b) → f a ≅ f b)
@ -1443,19 +1427,15 @@ protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk b :=
Quot.sound
@[reducible, elabAsEliminator]
protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
protected abbrev lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
Quot.lift f
@[elabAsEliminator]
protected theorem ind {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk a)) → (q : Quot Setoid.r) → motive q :=
Quot.ind
@[reducible, elabAsEliminator, inline]
protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
protected abbrev liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
Quot.liftOn q f c
@[elabAsEliminator]
protected theorem inductionOn {α : Sort u} [s : Setoid α] {motive : Quotient s → Prop}
(q : Quotient s)
(h : (a : α) → motive (Quotient.mk a))
@ -1478,24 +1458,21 @@ protected def rec
: motive q :=
Quot.rec f h q
@[reducible, elabAsEliminator, inline]
protected def recOn
protected abbrev recOn
(q : Quotient s)
(f : (a : α) → motive (Quotient.mk a))
(h : (a b : α) → (p : a ≈ b) → Eq.ndrec (f a) (Quotient.sound p) = f b)
: motive q :=
Quot.recOn q f h
@[reducible, elabAsEliminator, inline]
protected def recOnSubsingleton
protected abbrev recOnSubsingleton
[h : (a : α) → Subsingleton (motive (Quotient.mk a))]
(q : Quotient s)
(f : (a : α) → motive (Quotient.mk a))
: motive q :=
Quot.recOnSubsingleton (h := h) q f
@[reducible, elabAsEliminator, inline]
protected def hrecOn
protected abbrev hrecOn
(q : Quotient s)
(f : (a : α) → motive (Quotient.mk a))
(c : (a b : α) → (p : a ≈ b) → f a ≅ f b)
@ -1508,8 +1485,7 @@ universes uA uB uC
variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
variables [s₁ : Setoid α] [s₂ : Setoid β]
@[reducible, elabAsEliminator, inline]
protected def lift₂
protected abbrev lift₂
(f : α → β → φ)
(c : (a₁ : α) → (b₁ : β) → (a₂ : α) → (b₂ : β) → a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)
(q₁ : Quotient s₁) (q₂ : Quotient s₂)
@ -1519,8 +1495,7 @@ protected def lift₂
induction q₂ using Quotient.ind
apply c; assumption; apply Setoid.refl
@[reducible, elabAsEliminator, inline]
protected def liftOn₂
protected abbrev liftOn₂
(q₁ : Quotient s₁)
(q₂ : Quotient s₂)
(f : α → β → φ)
@ -1528,7 +1503,6 @@ protected def liftOn₂
: φ :=
Quotient.lift₂ f c q₁ q₂
@[elabAsEliminator]
protected theorem ind₂
{motive : Quotient s₁ → Quotient s₂ → Prop}
(h : (a : α) → (b : β) → motive (Quotient.mk a) (Quotient.mk b))
@ -1539,7 +1513,6 @@ protected theorem ind₂
induction q₂ using Quotient.ind
apply h
@[elabAsEliminator]
protected theorem inductionOn₂
{motive : Quotient s₁ → Quotient s₂ → Prop}
(q₁ : Quotient s₁)
@ -1550,7 +1523,6 @@ protected theorem inductionOn₂
induction q₂ using Quotient.ind
apply h
@[elabAsEliminator]
protected theorem inductionOn₃
[s₃ : Setoid φ]
{motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop}
@ -1594,8 +1566,7 @@ universes uA uB uC
variables {α : Sort uA} {β : Sort uB}
variables [s₁ : Setoid α] [s₂ : Setoid β]
@[reducible, elabAsEliminator]
protected def recOnSubsingleton₂
protected abbrev recOnSubsingleton₂
{motive : Quotient s₁ → Quotient s₂ → Sort uC}
[s : (a : α) → (b : β) → Subsingleton (motive (Quotient.mk a) (Quotient.mk b))]
(q₁ : Quotient s₁)

2
stage0/src/Init/Data/Nat/Div.lean generated
View file

@ -33,7 +33,6 @@ private theorem div.induction.F.{u}
(x : Nat) (f : ∀ (x₁ : Nat), x₁ < x → ∀ (y : Nat), C x₁ y) (y : Nat) : C x y :=
if h : 0 < y ∧ y ≤ x then h₁ x y h (f (x - y) (divRecLemma h) y) else h₂ x y h
@[elabAsEliminator]
theorem div.inductionOn.{u}
{motive : Nat → Nat → Sort u}
(x y : Nat)
@ -57,7 +56,6 @@ private theorem modDefAux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x
theorem modDef (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
difEqIf (0 < y ∧ y ≤ x) ((x - y) % y) x ▸ modDefAux x y
@[elabAsEliminator]
theorem mod.inductionOn.{u}
{motive : Nat → Nat → Sort u}
(x y : Nat)

6
stage0/src/Init/WF.lean generated
View file

@ -13,14 +13,12 @@ set_option codegen false
inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x
@[elabAsEliminator, inline, reducible]
def Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
(m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
{a : α} (n : Acc r a) : C a :=
Acc.rec (motive := fun α _ => C α) m n
@[elabAsEliminator, inline, reducible]
def Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
{a : α} (n : Acc r a)
(m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
: C a :=

8
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -358,13 +358,7 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
| _ => throwError "unexpected parentheses notation"
@[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
tryPostponeIfNoneOrMVar expectedType?
let some expectedType ← pure expectedType? |
throwError! "invalid `▸` notation, expected type must be known"
let expectedType ← instantiateMVars expectedType
if expectedType.hasExprMVar then
tryPostpone
throwError! "invalid `▸` notation, expected type contains metavariables{indentExpr expectedType}"
let expectedType ← tryPostponeIfHasMVars expectedType? "invalid `▸` notation"
match_syntax stx with
| `($heq ▸ $h) => do
let heq ← elabTerm heq none

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

@ -29,7 +29,7 @@ private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
| none => withMainMVarContext $ elabTerm major none
| some h => withMainMVarContext do
let lctx ← getLCtx
let x := lctx.getUnusedName `x
let x ← mkFreshUserName `x
let major ← elabTerm major none
evalGeneralizeAux h? major x
withMainMVarContext do
@ -74,7 +74,7 @@ private def generalizeVars (stx : Syntax) (major : Expr) : TacticM Nat := do
pure (fvarIds.size, [mvarId'])
private def getAlts (withAlts : Syntax) : Array Syntax :=
withAlts[2].getSepArgs
withAlts[1].getSepArgs
/-
Given an `inductionAlt` of the form

10
stage0/src/Lean/Elab/Term.lean generated
View file

@ -815,6 +815,16 @@ def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit :=
| some e => tryPostponeIfMVar e
| none => tryPostpone
def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?
let some expectedType ← pure expectedType? |
throwError! "{msg}, expected type must be known"
let expectedType ← instantiateMVars expectedType
if expectedType.hasExprMVar then
tryPostpone
throwError! "{msg}, expected type contains metavariables{indentExpr expectedType}"
pure expectedType
private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
trace[Elab.postpone]! "{stx} : {expectedType?}"
let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque

2
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -62,7 +62,7 @@ def majorPremise := parser! optional («try» (ident >> " : ")) >> termParser
def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
def inductionAlt : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
def inductionAlts : Parser := withPosition $ "| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
def withAlts : Parser := optional (" with " >> inductionAlts)
def withAlts : Parser := optional inductionAlts
def usingRec : Parser := optional (" using " >> ident)
def generalizingVars := optional (" generalizing " >> many1 ident)
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts

46
stage0/stdlib/Init/Core.c generated
View file

@ -17,7 +17,6 @@ lean_object* l_Init_Core___instance__51(lean_object*, lean_object*);
lean_object* l_strictAnd___boxed(lean_object*, lean_object*);
uint8_t l_Init_Core___instance__17;
lean_object* l_Init_Core___instance__8_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1(lean_object*, lean_object*);
lean_object* lean_thunk_map(lean_object*, lean_object*);
lean_object* l_Init_Core___instance__29___rarg(lean_object*, lean_object*);
lean_object* l_condEq___rarg(uint8_t, lean_object*, lean_object*);
@ -25,7 +24,6 @@ lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__43_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_reduceBool(uint8_t);
lean_object* l_Init_Core___instance__52___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_inline(lean_object*);
lean_object* l_Quotient_lift_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__7_match__1(lean_object*, lean_object*, lean_object*);
@ -73,6 +71,7 @@ lean_object* l_Init_Core___instance__5_match__1___rarg(lean_object*, lean_object
lean_object* l_Subtype_Init_Core___instance__42_match__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__27___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_idDelta___rarg(lean_object*);
lean_object* l_Init_Core___instance__52___boxed(lean_object*, lean_object*);
lean_object* l_Quot_liftOn___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_id___rarg___boxed(lean_object*);
lean_object* l_Init_Core___instance__9(lean_object*, lean_object*);
@ -124,7 +123,7 @@ uint8_t l_and(uint8_t, uint8_t);
lean_object* l_Quot_rec___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Quotient_lift_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Task_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__52(lean_object*);
lean_object* l_Init_Core___instance__52(lean_object*, lean_object*);
lean_object* lean_thunk_pure(lean_object*);
lean_object* l_Init_Core___instance__7(lean_object*, lean_object*);
lean_object* l_Nat_prio___closed__1;
@ -186,7 +185,7 @@ lean_object* l_flip___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__15(lean_object*);
lean_object* l_Quotient_hrecOn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Subtype_Init_Core___instance__42_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Init_Core___instance__52___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__52___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__27_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Quotient_rec(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__45_match__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -331,7 +330,6 @@ lean_object* l_Decidable_byCases___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__13_loop(lean_object*);
lean_object* l_prodHasDecidableLt(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_decidableOfDecidableOfIff___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_flip(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__2;
uint8_t l_Init_Core___instance__16;
@ -394,7 +392,6 @@ lean_object* l_Quotient_recOn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Decidable_decide(lean_object*);
lean_object* l_Quot_recOn(lean_object*, lean_object*, lean_object*);
lean_object* l_std_prec_maxPlus___closed__1;
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Init_Core___instance__9_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Init_Core___instance__45(lean_object*, lean_object*);
lean_object* l_Quot_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
@ -4154,56 +4151,31 @@ lean_dec(x_2);
return x_6;
}
}
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Init_Core___instance__52___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_apply_2(x_3, x_1, x_2);
x_4 = lean_apply_2(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_Init_Core___instance__52(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1___rarg), 3, 0);
x_3 = lean_alloc_closure((void*)(l_Init_Core___instance__52___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Init_Core___instance__52___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Init_Core___instance__52(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Init_Core___instance__52___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Init_Core___instance__52___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Quotient_recOnSubsingleton_u2082___at_Init_Core___instance__52___spec__1(x_1, x_2);
x_3 = l_Init_Core___instance__52(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Init_Core___instance__52___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Init_Core___instance__52___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_1);
return x_5;
}
}
lean_object* l___private_Init_Core_0__funSetoid(lean_object* x_1, lean_object* x_2) {
_start:
{

1489
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -896,7 +896,6 @@ lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__3___closed__2;
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__12;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__5;
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult_match__1___rarg(uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
lean_object* l_Lean_Elab_Term_Do_mkMatch(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_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkFreshJP___lambda__1___closed__1;
@ -1101,6 +1100,7 @@ extern lean_object* l_List_foldl___at_Lean_Meta_Match_Pattern_toMessageData___sp
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___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_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__16;
lean_object* l_Lean_Elab_Term_Do_mkTerminalAction(lean_object*);
extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__9;
@ -25477,7 +25477,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

4
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

@ -141,7 +141,6 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withDeclName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView_match__1(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_Lean_Elab_Term___instance__8___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__4;
@ -163,6 +162,7 @@ lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_LetRec_0__Lean_Elab_T
extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__2;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
lean_object* l___private_Lean_Elab_LetRec_0__Lean_Elab_Term_elabLetRecDeclValues(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkForallFVars___at_Lean_Elab_Term_elabForall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__2___closed__2;
@ -2690,7 +2690,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

4
stage0/stdlib/Lean/Elab/Tactic/Binders.c generated
View file

@ -78,7 +78,6 @@ lean_object* l___private_Lean_Elab_Tactic_Binders_0__Lean_Elab_Tactic_liftTermBi
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_expandShowTactic___closed__2;
extern lean_object* l_Lean_Init_LeanInit___instance__8___closed__1;
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
extern lean_object* l_Lean_mkAppStx___closed__9;
lean_object* l___private_Lean_Elab_Tactic_Binders_0__Lean_Elab_Tactic_liftTermBinderSyntax___closed__2;
extern lean_object* l_Lean_Level_LevelToFormat_toResult___closed__4;
@ -93,6 +92,7 @@ extern lean_object* l___regBuiltin_Lean_Elab_Term_elabSyntheticHole___closed__2;
lean_object* l_Lean_Elab_Tactic_expandShowTactic___closed__4;
lean_object* l___regBuiltin_Lean_Elab_Tactic_expandLetBangTactic(lean_object*);
lean_object* l_Lean_Elab_Tactic_expandShowTactic___closed__9;
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
lean_object* l___private_Lean_Elab_Tactic_Binders_0__Lean_Elab_Tactic_liftTermBinderSyntax___closed__6;
lean_object* l_Lean_Elab_Tactic_expandShowTactic___closed__2;
lean_object* l_Lean_Elab_Tactic_expandShowTactic___boxed(lean_object*, lean_object*, lean_object*);
@ -557,7 +557,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Tactics___hyg_31____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

159
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

@ -24,7 +24,6 @@ lean_object* lean_erase_macro_scopes(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkCasesResult_loop___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*);
lean_object* l_Lean_stringToMessageData(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalCases___spec__2(lean_object*, size_t, size_t, lean_object*);
lean_object* lean_local_ctx_get_unused_name(lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Elab_Tactic_withMainMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__4___closed__4;
@ -121,6 +120,7 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecIn
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecFromUsingLoop___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___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltCtorNames___spec__4(lean_object*, 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*);
@ -166,6 +166,7 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAlt
lean_object* l_Lean_Elab_Tactic_evalInduction_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfoDefault_match__5(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalInduction___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___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getGeneralizingFVarIds___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -185,6 +186,7 @@ lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_obj
lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_processResult___spec__1___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_Tactic_getInductiveValFromMajor___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
lean_object* l_Lean_Core_mkFreshUserName___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfoDefault___spec__1___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeMajor_match__2(lean_object*);
extern lean_object* l_Lean_mkSimpleThunk___closed__1;
@ -300,6 +302,7 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases___closed__1;
extern lean_object* l_Lean_Meta_Lean_Meta_Tactic_Induction___instance__1;
lean_object* l_Array_toList___rarg(lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Core_mkFreshUserName___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor_match__2(lean_object*);
uint8_t l_Std_Range_forIn_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo___spec__2___lambda__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfoDefault___closed__4;
@ -478,6 +481,14 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_
return x_2;
}
}
lean_object* l_Lean_Core_mkFreshUserName___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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) {
_start:
{
lean_object* x_11;
x_11 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_1, x_8, x_9, x_10);
return x_11;
}
}
static lean_object* _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__1___closed__1() {
_start:
{
@ -536,26 +547,31 @@ return x_17;
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__2(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:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20;
x_14 = l_Lean_Meta_mkArrow___rarg___closed__2;
x_15 = lean_local_ctx_get_unused_name(x_4, x_14);
x_16 = lean_box(0);
x_17 = 0;
x_15 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_14, x_11, x_12, x_13);
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);
x_18 = lean_box(0);
x_19 = 0;
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_18 = l_Lean_Elab_Tactic_elabTerm(x_1, x_16, x_17, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_18) == 0)
x_20 = l_Lean_Elab_Tactic_elabTerm(x_1, x_18, x_19, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_17);
if (lean_obj_tag(x_20) == 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_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -564,26 +580,26 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_15);
x_21 = l_Lean_Elab_Tactic_evalGeneralizeAux(x_2, x_19, x_15, 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_inc(x_16);
x_23 = l_Lean_Elab_Tactic_evalGeneralizeAux(x_2, x_21, x_16, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_22);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__1___boxed), 11, 1);
lean_closure_set(x_23, 0, x_15);
x_24 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_24, 0, x_3);
lean_closure_set(x_24, 1, x_23);
x_25 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_24, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_22);
return x_25;
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
x_25 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__1___boxed), 11, 1);
lean_closure_set(x_25, 0, x_16);
x_26 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___spec__1___rarg), 11, 2);
lean_closure_set(x_26, 0, x_3);
lean_closure_set(x_26, 1, x_25);
x_27 = l_Lean_Elab_Tactic_withMainMVarContext___rarg(x_26, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_24);
return x_27;
}
else
{
uint8_t x_26;
lean_dec(x_15);
uint8_t x_28;
lean_dec(x_16);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
@ -593,30 +609,30 @@ lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_26 = !lean_is_exclusive(x_21);
if (x_26 == 0)
x_28 = !lean_is_exclusive(x_23);
if (x_28 == 0)
{
return x_21;
return x_23;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_21, 0);
x_28 = lean_ctor_get(x_21, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_21);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_23, 0);
x_30 = lean_ctor_get(x_23, 1);
lean_inc(x_30);
lean_inc(x_29);
lean_dec(x_23);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
}
}
else
{
uint8_t x_30;
lean_dec(x_15);
uint8_t x_32;
lean_dec(x_16);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
@ -627,23 +643,23 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_30 = !lean_is_exclusive(x_18);
if (x_30 == 0)
x_32 = !lean_is_exclusive(x_20);
if (x_32 == 0)
{
return x_18;
return x_20;
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_18, 0);
x_32 = lean_ctor_get(x_18, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_18);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
return x_33;
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_20, 0);
x_34 = lean_ctor_get(x_20, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_20);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
@ -668,7 +684,7 @@ else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_17 = l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_sortFVarIds___closed__4;
x_18 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__2), 13, 3);
x_18 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__2___boxed), 13, 3);
lean_closure_set(x_18, 0, x_2);
lean_closure_set(x_18, 1, x_1);
lean_closure_set(x_18, 2, x_17);
@ -680,6 +696,22 @@ return x_20;
}
}
}
lean_object* l_Lean_Core_mkFreshUserName___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Core_mkFreshUserName___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___spec__1(x_1, 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);
return x_11;
}
}
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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:
{
@ -696,6 +728,15 @@ lean_dec(x_3);
return x_12;
}
}
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___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, lean_object* x_13) {
_start:
{
lean_object* x_14;
x_14 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabMajor___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_4);
return x_14;
}
}
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeMajor_match__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1539,7 +1580,7 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAlts(
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_unsigned_to_nat(2u);
x_2 = lean_unsigned_to_nat(1u);
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
x_4 = l_Lean_Syntax_getSepArgs(x_3);
lean_dec(x_3);

455
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -32,6 +32,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__1;
lean_object* l_Lean_mkAppStx(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Lean_Elab_Term___instance__13___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
@ -44,6 +45,7 @@ lean_object* l_Lean_Meta_inferType___at___private_Lean_Elab_Term_0__Lean_Elab_Te
lean_object* l_Lean_Meta_isType___at_Lean_Elab_Term_ensureType___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat___closed__11;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___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_Term_tryPostponeIfHasMVars_match__1(lean_object*);
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_foldlM___at_Lean_withNestedTraces___spec__1(lean_object*, lean_object*, lean_object*);
@ -125,6 +127,7 @@ lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___boxed(l
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__12___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3___closed__4;
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1;
@ -163,6 +166,7 @@ uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_isLambdaWithImplicit(lean_o
uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicit(lean_object*);
size_t l_USize_sub(size_t, size_t);
uint8_t lean_metavar_ctx_is_delayed_assigned(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4;
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -427,6 +431,7 @@ lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
lean_object* l_Lean_Elab_Term_mkFreshInstanceName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_read___at_Lean_Elab_Term_Lean_Elab_Term___instance__8___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__3;
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__3;
lean_object* l_Lean_Meta_getDecLevel___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -453,6 +458,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureExpectedType(lean_object*);
extern lean_object* l_Lean_Lean_Exception___instance__1___closed__1;
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_Lean_Elab_Term___instance__13___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -483,7 +489,6 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__1;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_getResetPostponed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
uint8_t l_Lean_MetavarContext_isWellFormed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Term_blockImplicitLambda(lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
@ -522,7 +527,7 @@ lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*,
lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443_(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567_(lean_object*);
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*);
lean_object* l_Lean_Elab_Term_getLetRecsToLift(lean_object*);
lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -656,6 +661,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__2;
extern lean_object* l_Lean_Meta_isLevelDefEq___rarg___lambda__2___closed__2;
lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveLocalName_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___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*);
lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -682,6 +688,7 @@ lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_trySynthInstanceIm
extern lean_object* l_Lean_Elab_addMacroStack___rarg___lambda__1___closed__3;
lean_object* l___private_Lean_Meta_Check_0__Lean_Meta_getFunctionDomain(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_addGlobalInstanceImp___closed__4;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2;
lean_object* l_Lean_Elab_Term_getDeclName_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Lean_Elab_Term___instance__13___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_setMacroStackOption(lean_object*, uint8_t);
@ -852,7 +859,6 @@ lean_object* l_Lean_Syntax_getPos(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Term_Lean_Elab_Term___instance__8___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMessageLog___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
lean_object* l_Lean_Elab_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
@ -862,6 +868,7 @@ lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__11;
lean_object* l_Lean_Meta_decLevel___at_Lean_Meta_getDecLevel___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__11___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabQuotedName(lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
extern lean_object* l_Lean_Elab_abortExceptionId;
lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__11;
@ -890,6 +897,7 @@ extern lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_NameGenerator_Init_LeanInit___instance__6___closed__1;
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3;
lean_object* l_Lean_Meta_mkFreshLevelMVar___at_Lean_Elab_Term_ensureType___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getLetRecsToLift___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__1;
@ -971,7 +979,7 @@ lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_
lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_isLevelDefEq___rarg___lambda__2___closed__4;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332_(lean_object*);
lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__3(lean_object*, size_t, size_t, lean_object*);
extern lean_object* l_Lean_Expr_Lean_Expr___instance__11___closed__1;
@ -1028,6 +1036,7 @@ lean_object* l_Nat_foldM_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mk
lean_object* lean_local_ctx_find(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_isLetRecAuxMVar___closed__5;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe(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_Term_tryPostponeIfHasMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__2(lean_object*, lean_object*);
lean_object* lean_usize_to_nat(size_t);
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__3;
@ -1057,11 +1066,11 @@ lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__8___closed__5;
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_resolveName___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_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
lean_object* l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabQuotedName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__6;
lean_object* l_Lean_Elab_Term_resolveName___closed__1;
lean_object* l_Lean_Elab_Term_mkAuxName___closed__1;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1;
lean_object* l_Lean_Elab_Term_isLocalIdent_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_SMap_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__1___boxed(lean_object*, lean_object*);
@ -20570,6 +20579,394 @@ lean_dec(x_2);
return x_9;
}
}
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_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_dec(x_2);
x_4 = lean_apply_1(x_3, x_1);
return x_4;
}
else
{
lean_object* x_5; lean_object* x_6;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_apply_1(x_2, x_5);
return x_6;
}
}
}
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_tryPostponeIfHasMVars_match__1___rarg), 3, 0);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(", expected type must be known");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(", expected type contains metavariables");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars(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) {
_start:
{
lean_object* x_10;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_1);
x_10 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_10) == 0)
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_stringToMessageData(x_2);
x_13 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
x_14 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_12);
x_15 = l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2;
x_16 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_16, x_3, x_4, x_5, x_6, x_7, x_8, x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_10, 1);
lean_inc(x_18);
lean_dec(x_10);
x_19 = lean_ctor_get(x_1, 0);
lean_inc(x_19);
lean_dec(x_1);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_20 = l_Lean_Meta_instantiateMVarsImp(x_19, x_5, x_6, x_7, x_8, x_18);
if (lean_obj_tag(x_20) == 0)
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_20, 0);
x_23 = lean_ctor_get(x_20, 1);
x_24 = l_Lean_Expr_hasExprMVar(x_22);
if (x_24 == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
return x_20;
}
else
{
lean_object* x_25;
lean_free_object(x_20);
x_25 = l_Lean_Elab_Term_tryPostpone(x_3, x_4, x_5, x_6, x_7, x_8, 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; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = l_Lean_stringToMessageData(x_2);
x_28 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
x_29 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_27);
x_30 = l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4;
x_31 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
x_32 = l_Lean_indentExpr(x_22);
x_33 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_28);
x_35 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_26);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
{
return x_35;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_35, 0);
x_38 = lean_ctor_get(x_35, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_35);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
else
{
uint8_t x_40;
lean_dec(x_22);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_40 = !lean_is_exclusive(x_25);
if (x_40 == 0)
{
return x_25;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_25, 0);
x_42 = lean_ctor_get(x_25, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_25);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
}
else
{
lean_object* x_44; lean_object* x_45; uint8_t x_46;
x_44 = lean_ctor_get(x_20, 0);
x_45 = lean_ctor_get(x_20, 1);
lean_inc(x_45);
lean_inc(x_44);
lean_dec(x_20);
x_46 = l_Lean_Expr_hasExprMVar(x_44);
if (x_46 == 0)
{
lean_object* x_47;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_44);
lean_ctor_set(x_47, 1, x_45);
return x_47;
}
else
{
lean_object* x_48;
x_48 = l_Lean_Elab_Term_tryPostpone(x_3, x_4, x_5, x_6, x_7, x_8, x_45);
if (lean_obj_tag(x_48) == 0)
{
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; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
x_50 = l_Lean_stringToMessageData(x_2);
x_51 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__1;
x_52 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
x_53 = l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4;
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_indentExpr(x_44);
x_56 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_57, 0, x_56);
lean_ctor_set(x_57, 1, x_51);
x_58 = l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(x_57, x_3, x_4, x_5, x_6, x_7, x_8, x_49);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_59 = lean_ctor_get(x_58, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_58, 1);
lean_inc(x_60);
if (lean_is_exclusive(x_58)) {
lean_ctor_release(x_58, 0);
lean_ctor_release(x_58, 1);
x_61 = x_58;
} else {
lean_dec_ref(x_58);
x_61 = lean_box(0);
}
if (lean_is_scalar(x_61)) {
x_62 = lean_alloc_ctor(1, 2, 0);
} else {
x_62 = x_61;
}
lean_ctor_set(x_62, 0, x_59);
lean_ctor_set(x_62, 1, x_60);
return x_62;
}
else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
lean_dec(x_44);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_63 = lean_ctor_get(x_48, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_48, 1);
lean_inc(x_64);
if (lean_is_exclusive(x_48)) {
lean_ctor_release(x_48, 0);
lean_ctor_release(x_48, 1);
x_65 = x_48;
} else {
lean_dec_ref(x_48);
x_65 = lean_box(0);
}
if (lean_is_scalar(x_65)) {
x_66 = lean_alloc_ctor(1, 2, 0);
} else {
x_66 = x_65;
}
lean_ctor_set(x_66, 0, x_63);
lean_ctor_set(x_66, 1, x_64);
return x_66;
}
}
}
}
else
{
uint8_t x_67;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_67 = !lean_is_exclusive(x_20);
if (x_67 == 0)
{
return x_20;
}
else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_20, 0);
x_69 = lean_ctor_get(x_20, 1);
lean_inc(x_69);
lean_inc(x_68);
lean_dec(x_20);
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_68);
lean_ctor_set(x_70, 1, x_69);
return x_70;
}
}
}
}
else
{
uint8_t x_71;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
x_71 = !lean_is_exclusive(x_10);
if (x_71 == 0)
{
return x_10;
}
else
{
lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_72 = lean_ctor_get(x_10, 0);
x_73 = lean_ctor_get(x_10, 1);
lean_inc(x_73);
lean_inc(x_72);
lean_dec(x_10);
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_72);
lean_ctor_set(x_74, 1, x_73);
return x_74;
}
}
}
}
lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___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) {
_start:
{
lean_object* x_10;
x_10 = l_Lean_Elab_Term_tryPostponeIfHasMVars(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_4);
lean_dec(x_2);
return x_10;
}
}
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___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) {
_start:
{
@ -28937,7 +29334,7 @@ lean_dec(x_3);
return x_9;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1() {
_start:
{
lean_object* x_1;
@ -28945,21 +29342,21 @@ x_1 = lean_mk_string("letrec");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2() {
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_834____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -29126,7 +29523,7 @@ lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean
x_89 = lean_ctor_get(x_83, 1);
lean_inc(x_89);
lean_dec(x_83);
x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
x_91 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_90, x_2, x_3, x_4, x_5, x_6, x_7, x_89);
x_92 = lean_ctor_get(x_91, 0);
lean_inc(x_92);
@ -29168,7 +29565,7 @@ lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean
x_49 = lean_ctor_get(x_43, 1);
lean_inc(x_49);
lean_dec(x_43);
x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
x_51 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_50, x_2, x_3, x_4, x_5, x_6, x_7, x_49);
x_52 = lean_ctor_get(x_51, 0);
lean_inc(x_52);
@ -29245,7 +29642,7 @@ x_37 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
x_38 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
x_40 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_39, x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_32);
x_41 = lean_ctor_get(x_40, 1);
lean_inc(x_41);
@ -29303,7 +29700,7 @@ x_73 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
x_74 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_74, 0, x_72);
lean_ctor_set(x_74, 1, x_73);
x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2;
x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2;
x_76 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_75, x_74, x_2, x_3, x_4, x_5, x_6, x_7, x_57);
x_77 = lean_ctor_get(x_76, 1);
lean_inc(x_77);
@ -36539,7 +36936,7 @@ x_8 = l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg(x_1, x_2, x_3, x_4,
return x_8;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -36549,7 +36946,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -36561,7 +36958,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
@ -36922,6 +37319,14 @@ l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__8 = _init_l
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__8);
l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__9 = _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__9();
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__9);
l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1 = _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__1);
l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2 = _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2);
l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3 = _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__3);
l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4 = _init_l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__4);
l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___closed__1 = _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___closed__1);
l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___closed__1 = _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___closed__1();
@ -37004,11 +37409,11 @@ l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___clos
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2);
l_Lean_Elab_Term_mkAuxName___closed__3 = _init_l_Lean_Elab_Term_mkAuxName___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__3);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5443_(lean_io_mk_world());
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__1);
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2();
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567____closed__2);
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5567_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_isLetRecAuxMVar___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___closed__1();
@ -37227,9 +37632,9 @@ l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__2 = _init_l_Lean
lean_mark_persistent(l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__2);
l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3 = _init_l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7208_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332____closed__1);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7332_(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));

82
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -214,7 +214,6 @@ lean_object* l_Lean_Parser_Tactic_failIfSuccess_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_orelse_parenthesizer___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_refine_x21_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Tactic_match_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_changeWith___elambda__1___closed__1;
@ -234,7 +233,6 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__8;
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_apply_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_generalizingVars_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_withAlts___closed__4;
lean_object* l_Lean_Parser_Tactic_locationHyp_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_rewrite___closed__6;
lean_object* l_Lean_Parser_Tactic_location___closed__3;
@ -259,7 +257,6 @@ lean_object* l_Lean_Parser_Tactic_inductionAlts;
lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_revert_formatter___closed__1;
lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_cases_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_let___closed__2;
@ -1854,7 +1851,6 @@ lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__9;
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Tactic_apply_parenthesizer(lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_refine(lean_object*);
lean_object* l_Lean_Parser_Tactic_withAlts_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_inductionAlt_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__7;
@ -14517,23 +14513,11 @@ x_1 = l_Lean_Parser_Tactic_inductionAlts___closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_structInst___elambda__1___closed__5;
x_2 = l_Lean_Parser_Tactic_inductionAlts___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_withAlts___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1;
x_3 = l_Lean_Parser_Tactic_inductionAlts___closed__5;
x_4 = l_Lean_Parser_optionalFn(x_3, x_1, x_2);
return x_4;
}
@ -14541,38 +14525,28 @@ return x_4;
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_inductionAlts;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_structInst___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
x_3 = l_Lean_Parser_optionaInfo(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_withAlts___closed__1;
x_2 = l_Lean_Parser_optionaInfo(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_withAlts___elambda__1), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___closed__4() {
static lean_object* _init_l_Lean_Parser_Tactic_withAlts___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_withAlts___closed__2;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__3;
x_1 = l_Lean_Parser_Tactic_withAlts___closed__1;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -14583,7 +14557,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_withAlts() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_withAlts___closed__4;
x_1 = l_Lean_Parser_Tactic_withAlts___closed__3;
return x_1;
}
}
@ -14880,7 +14854,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_generalizingVars___closed__4;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__3;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -15361,23 +15335,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_inductionAlts_formatter),
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_structInst_formatter___closed__2;
x_2 = l_Lean_Parser_Tactic_withAlts_formatter___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_withAlts_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_Parser_Tactic_withAlts_formatter___closed__2;
x_6 = l_Lean_Parser_Tactic_withAlts_formatter___closed__1;
x_7 = l_Lean_PrettyPrinter_Formatter_visitArgs(x_6, x_1, x_2, x_3, x_4, x_5);
return x_7;
}
@ -15811,23 +15773,11 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_inductionAlts_parenthesize
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_structInst_parenthesizer___closed__2;
x_2 = l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_withAlts_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2;
x_6 = l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1;
x_7 = l_Lean_PrettyPrinter_Parenthesizer_visitArgs(x_6, x_1, x_2, x_3, x_4, x_5);
return x_7;
}
@ -16054,7 +16004,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_majorPremise___closed__5;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__3;
x_2 = l_Lean_Parser_Tactic_withAlts___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -22909,16 +22859,12 @@ l_Lean_Parser_Tactic_inductionAlts___closed__6 = _init_l_Lean_Parser_Tactic_indu
lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlts___closed__6);
l_Lean_Parser_Tactic_inductionAlts = _init_l_Lean_Parser_Tactic_inductionAlts();
lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlts);
l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts___elambda__1___closed__1);
l_Lean_Parser_Tactic_withAlts___closed__1 = _init_l_Lean_Parser_Tactic_withAlts___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts___closed__1);
l_Lean_Parser_Tactic_withAlts___closed__2 = _init_l_Lean_Parser_Tactic_withAlts___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts___closed__2);
l_Lean_Parser_Tactic_withAlts___closed__3 = _init_l_Lean_Parser_Tactic_withAlts___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts___closed__3);
l_Lean_Parser_Tactic_withAlts___closed__4 = _init_l_Lean_Parser_Tactic_withAlts___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts___closed__4);
l_Lean_Parser_Tactic_withAlts = _init_l_Lean_Parser_Tactic_withAlts();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts);
l_Lean_Parser_Tactic_usingRec___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_usingRec___elambda__1___closed__1();
@ -23052,8 +22998,6 @@ l_Lean_Parser_Tactic_inductionAlts_formatter___closed__4 = _init_l_Lean_Parser_T
lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlts_formatter___closed__4);
l_Lean_Parser_Tactic_withAlts_formatter___closed__1 = _init_l_Lean_Parser_Tactic_withAlts_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts_formatter___closed__1);
l_Lean_Parser_Tactic_withAlts_formatter___closed__2 = _init_l_Lean_Parser_Tactic_withAlts_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts_formatter___closed__2);
l_Lean_Parser_Tactic_induction_formatter___closed__1 = _init_l_Lean_Parser_Tactic_induction_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_induction_formatter___closed__1);
l_Lean_Parser_Tactic_induction_formatter___closed__2 = _init_l_Lean_Parser_Tactic_induction_formatter___closed__2();
@ -23121,8 +23065,6 @@ l_Lean_Parser_Tactic_inductionAlts_parenthesizer___closed__5 = _init_l_Lean_Pars
lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlts_parenthesizer___closed__5);
l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1);
l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__2);
l_Lean_Parser_Tactic_induction_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_induction_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_induction_parenthesizer___closed__1);
l_Lean_Parser_Tactic_induction_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_induction_parenthesizer___closed__2();