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 2022-04-05 17:38:43 -07:00
parent eae4b92b0d
commit d65691626c
38 changed files with 15736 additions and 4684 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
stage0/src/Init/Classical.lean generated
View file

@ -22,7 +22,7 @@ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :
theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
/-- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
@ -90,8 +90,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
⟨xp.val, fun h' => xp.property⟩)
(fun hp => ⟨choice h, fun h => absurd h hp⟩)
/- the Hilbert epsilon Function -/
/-- the Hilbert epsilon Function -/
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
(strongIndefiniteDescription p h).val
@ -104,8 +103,7 @@ theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@ep
theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
@epsilon_spec α (fun y => y = x) ⟨x, rfl⟩
/- the axiom of choice -/
/-- the axiom of choice -/
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x) :=
⟨_, fun x => choose_spec (h x)⟩
@ -125,9 +123,21 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
Decidable.byContradiction (dec := propDecidable _) h
macro "by_cases" h:ident ":" e:term : tactic =>
`(cases em $e:term with
| inl $h:ident => _
| inr $h:ident => _)
/--
`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
-/
syntax "by_cases" (atomic(ident ":"))? term : tactic
macro_rules
| `(tactic| by_cases $h:ident : $e:term) =>
`(tactic|
cases em $e:term with
| inl $h:ident => _
| inr $h:ident => _)
| `(tactic| by_cases $e:term) =>
`(tactic|
cases em $e:term with
| inl h => _
| inr h => _)
end Classical

6
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -628,8 +628,10 @@ def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
rw [size_set, size_set]
@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 :=
List.length_dropLast ..
@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
match a with
| ⟨[]⟩ => rfl
| ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub]
def popWhile (p : α → Bool) (as : Array α) : Array α :=
if h : as.size > 0 then

14
stage0/src/Init/Data/Array/Mem.lean generated
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Data.Array.Basic
import Init.Data.Nat.Linear
import Init.Data.List.BasicAux
theorem List.sizeOf_get_lt [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
match as, i with
@ -40,4 +41,17 @@ theorem sizeOf_lt_of_mem [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈
apply aux 0 h
termination_by aux j _ => as.size - j
@[simp] theorem sizeOf_get [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
cases as
simp [get]
apply Nat.lt_trans (List.sizeOf_get ..)
simp_arith
macro "array_get_dec" : tactic =>
`(first
| apply sizeOf_get
| apply Nat.lt_trans (sizeOf_get ..); simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
end Array

8
stage0/src/Init/Data/List/Basic.lean generated
View file

@ -485,14 +485,12 @@ def dropLast {α} : List α → List α
| zero => rfl
| succ i => simp [set, ih]
@[simp] theorem length_dropLast (as : List α) : as.dropLast.length = as.length - 1 := by
@[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
match as with
| [] => rfl
| [a] => rfl
| a::b::as =>
have ih := length_dropLast (b::as)
| b::bs =>
have ih := length_dropLast_cons b bs
simp[dropLast, ih]
rfl
@[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
induction as with

17
stage0/src/Init/Data/List/BasicAux.lean generated
View file

@ -121,6 +121,15 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
| head => simp_arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
macro "sizeOf_list_dec" : tactic =>
`(first
| apply sizeOf_lt_of_mem; assumption; done
| apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs := by
induction as with
| nil => assumption
@ -145,4 +154,12 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
next => apply append_cancel_right
next => intro h; simp [h]
@[simp] theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
match as, i with
| a::as, ⟨0, _⟩ => simp_arith [get]
| a::as, ⟨i+1, h⟩ =>
have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
apply Nat.lt_trans ih
simp_arith
end List

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

@ -301,6 +301,8 @@ theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by
| 0 => contradiction
| a+1 => apply Nat.zero_lt_succ
attribute [simp] Nat.lt_irrefl
theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
fun he => absurd (he ▸ h) (Nat.lt_irrefl a)

28
stage0/src/Init/Data/Range.lean generated
View file

@ -14,6 +14,9 @@ structure Range where
stop : Nat
step : Nat := 1
instance : Membership Nat Range where
mem i r := r.start ≤ i ∧ i < r.stop
namespace Range
universe u v
@ -21,7 +24,7 @@ universe u v
-- pass `stop` and `step` separately so the `range` object can be eliminated through inlining
let rec @[specialize] loop (fuel i stop step : Nat) (b : β) : m β := do
if i ≥ stop then
pure b
return b
else match fuel with
| 0 => pure b
| fuel+1 => match (← f i b) with
@ -32,6 +35,21 @@ universe u v
instance : ForIn m Range Nat where
forIn := Range.forIn
@[inline] protected def forIn' {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=
let rec @[specialize] loop (start stop step : Nat) (f : (i : Nat) → start ≤ i ∧ i < stop → β → m (ForInStep β)) (fuel i : Nat) (hl : start ≤ i) (b : β) : m β := do
if hu : i < stop then
match fuel with
| 0 => pure b
| fuel+1 => match (← f i ⟨hl, hu⟩ b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop start stop step f fuel (i + step) (Nat.le_trans hl (Nat.le_add_right ..)) b
else
return b
loop range.start range.stop range.step f range.stop range.start (Nat.le_refl ..) init
instance : ForIn' m Range Nat inferInstance where
forIn' := Range.forIn'
@[inline] protected def forM {m : Type u → Type v} [Monad m] (range : Range) (f : Nat → m PUnit) : m PUnit :=
let rec @[specialize] loop (fuel i stop step : Nat) : m PUnit := do
if i ≥ stop then
@ -57,3 +75,11 @@ macro_rules
end Range
end Std
theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := by
simp [Membership.mem] at h
exact h.2
theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := by
simp [Membership.mem] at h
exact h.1

122
stage0/src/Init/Notation.lean generated
View file

@ -293,6 +293,12 @@ syntax (name := constructor) "constructor" : tactic
`case tag => tac` focuses on the goal with case name `tag` and solves it using `tac`, or else fails.
`case tag x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/
syntax (name := case) "case " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic
/--
Similar to the `case tag => tac` tactic but for writing macros. Recall that `case` closes the goal using `sorry` when it fails,
and the tactic execution is not interrupted.
-/
syntax (name := case') "case' " (ident <|> "_") (ident <|> "_")* " => " tacticSeq : tactic
/--
`next => tac` focuses on the next goal solves it using `tac`, or else fails.
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with inaccessible names to the given names. -/
@ -310,8 +316,11 @@ syntax (name := focus) "focus " tacticSeq : tactic
syntax (name := skip) "skip" : tactic
/-- `done` succeeds iff there are no remaining goals. -/
syntax (name := done) "done" : tactic
/-- This tactic displays the current state in the info view. -/
syntax (name := traceState) "trace_state" : tactic
/-- `trace msg` displays `msg` in the info view. -/
syntax (name := traceMessage) "trace " str : tactic
/-- Fails if the given tactic succeeds. -/
syntax (name := failIfSuccess) "fail_if_success " tacticSeq : tactic
syntax (name := paren) "(" tacticSeq ")" : tactic
syntax (name := withReducible) "with_reducible " tacticSeq : tactic
@ -340,6 +349,7 @@ syntax (name := ac_refl) "ac_refl " : tactic
macro "admit" : tactic => `(exact sorry)
/-- The `sorry` tactic is a shorthand for `exact sorry`. -/
macro "sorry" : tactic => `(exact sorry)
/-- `infer_instance` is an abbreviation for `exact inferInstance` -/
macro "infer_instance" : tactic => `(exact inferInstance)
/-- Optional configuration option for tactics -/
@ -355,8 +365,18 @@ syntax (name := changeWith) "change " term " with " term (location)? : tactic
syntax rwRule := ("← " <|> "<- ")? term
syntax rwRuleSeq := "[" rwRule,*,? "]"
/--
`rewrite [e]` applies identity `e` as a rewrite rule to the target of the main goal.
If `e` is preceded by left arrow (`←` or `<-`), the rewrite is applied in the reverse direction.
If `e` is a defined constant, then the equational theorems associated with `e` are used. This provides a convenient way to unfold `e`.
- `rewrite [e₁, ..., eₙ]` applies the given rules sequentially.
- `rewrite [e] at l` rewrites `e` at location(s) `l`, where `l` is either `*` or a list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-` can also be used, to signify the target of the goal.
-/
syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic
/--
An abbreviation for `rewrite`.
-/
syntax (name := rwSeq) "rw " (config)? rwRuleSeq (location)? : tactic
def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Syntax := do
@ -371,8 +391,17 @@ def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Sy
@[macro rwSeq] def expandRwSeq : Macro :=
rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
/--
The `injection` tactic is based on the fact that constructors of inductive data types are injections.
That means that if `c` is a constructor of an inductive datatype, and if `(c t₁)` and `(c t₂)` are two terms that are equal then `t₁` and `t₂` are equal too.
If `q` is a proof of a statement of conclusion `t₁ = t₂`, then injection applies injectivity to derive the equality of all arguments of `t₁` and `t₂`
placed in the same positions. For example, from `(a::b) = (c::d)` we derive `a=c` and `b=d`. To use this tactic `t₁` and `t₂`
should be constructor applications of the same constructor.
Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types `a = c` and `b = d` to the main goal.
The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses.
-/
syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
-- TODO: add with
syntax (name := injections) "injections" : tactic
syntax discharger := atomic("(" (&"discharger" <|> &"disch")) " := " tacticSeq ")"
@ -382,7 +411,23 @@ syntax simpPost := "↑"
syntax simpLemma := (simpPre <|> simpPost)? ("← " <|> "<- ")? term
syntax simpErase := "-" term:max
syntax simpStar := "*"
/--
The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants.
- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.
- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions. If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with `f` are used. This provides a convenient way to unfold `f`.
- `simp [*]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and all hypotheses.
- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas
- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`, but removes the ones named `idᵢ`.
- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis `hᵢ` is introduced, but the old one remains in the local context.
- `simp at *` simplifies all the hypotheses and the target.
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the other hypotheses.
-/
syntax (name := simp) "simp " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/--
A stronger version of `simp [*] at *` where the hypotheses and target are simplified
multiple times until no simplication is applicable.
Only non-dependent propositional hypotheses are considered.
-/
syntax (name := simpAll) "simp_all " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
/--
@ -399,12 +444,38 @@ syntax (name := unfold) "unfold " ident (location)? : tactic
-- It makes sure the "continuation" `?_` is the main goal after refining
macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right))
/--
`have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term of type `t`. If `t` is omitted, it will be inferred.
If `h` is omitted, the name `this` is used.
The variant `have pattern := e` is equivalent to `match e with | pattern => _`, and it is convenient for types that have only applicable constructor.
Example: given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
-/
macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
/- We use a priority > default, to avoid ambiguity with previous `have` notation -/
/--
`have h := e` adds the hypothesis `h : t` if `e : t`.
-/
macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
/--
Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`,
`e` must have type `t` in the context `ctx, h : t'`.
The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
If `h :` is omitted, the name `this` is used.
-/
macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d:sufficesDecl; ?_)
/--
`let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`.
If `t` is omitted, it will be inferred.
The variant `let pattern := e` is equivalent to `match e with | pattern => _`, and it is convenient for types that have only applicable constructor.
Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
-/
macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
macro "show " e:term : tactic => `(refine_lift show $e:term from ?_)
/--
`show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
performs the unification, and replaces the target with the unified version of `t`.
-/
macro "show " e:term : tactic => `(refine_lift show $e:term from ?_) -- TODO: fix, see comment
syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
macro_rules
| `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
@ -417,6 +488,20 @@ macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
syntax inductionAlt := ppDedent(ppLine) "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
/--
Assuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal,
producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor
and an inductive hypothesis is added for each recursive argument to the constructor.
If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward,
so that the inductive hypothesis incorporates that hypothesis as well.
For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal
with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`.
Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor.
- `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable.
- `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
- `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.
- Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.
-/
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident
@ -426,6 +511,17 @@ If `h` is given, `h : e = x` is introduced as well. -/
syntax (name := generalize) "generalize " generalizeArg,+ : tactic
syntax casesTarget := atomic(ident " : ")? term
/--
Assuming `x` is a variable in the local context with an inductive type, `cases x` splits the main goal,
producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor.
If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward,
so that the case split affects that hypothesis as well. `cases` detects unreachable cases and closes them automatically.
For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `cases n` produces one goal with hypothesis `h : P 0` and target `Q 0`,
and one goal with hypothesis `h : P (Nat.succ a)` and target `Q (Nat.succ a)`. Here the name `a` is chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor.
- `cases e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then cases on the resulting variable.
- Given `as : List α`, `cases as with | nil => tac₁ | cons a as' => tac₂`, uses tactic `tac₁` for the `nil` case, and `tac₂` for the `cons` case, and `a` and `as'` are used as names for the new variables introduced.
- `cases h : e`, where `e` is a variable or an expression, performs cases on `e` as above, but also adds a hypothesis `h : e = ...` to each hypothesis, where `...` is the constructor instance for that particular case.
-/
syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
syntax (name := existsIntro) "exists " term : tactic
@ -433,16 +529,35 @@ syntax (name := existsIntro) "exists " term : tactic
/-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
syntax (name := renameI) "rename_i " (colGt (ident <|> "_"))+ : tactic
/--
`repeat tac` applies `tac` to main goal. If the application succeeds,
the tactic is applied recursively to the generated subgoals until it eventually fails.
-/
syntax "repeat " tacticSeq : tactic
macro_rules
| `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)
/--
Tries different simple tactics (e.g., `rfl`, `contradiction`, ...) to close the current goal.
You can use the command `macro_rules` to extend the set of tactics used. Example:
```
macro_rules | `(tactic| trivial) => `(tactic| simp)
```
-/
syntax "trivial" : tactic
/--
The `split` tactic is useful for breaking nested if-then-else and match expressions in cases.
For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals
-/
syntax (name := split) "split " (colGt term)? (location)? : tactic
syntax (name := dbgTrace) "dbg_trace " str : tactic
/-- Helper tactic for "discarding" the rest of a proof. It is useful when working on the middle of a complex proofs,
and less messy than commenting the remainder of the proof. -/
macro "stop" s:tacticSeq : tactic => `(repeat sorry)
/--
The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`.
The premises of this hypothesis, either universal quantifications or non-dependent implications,
@ -459,6 +574,7 @@ macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t:tacticSeq)
/-- `fail msg` is a tactic that always fail and produces an error using the given message. -/
syntax (name := fail) "fail " (str)? : tactic
syntax (name := checkpoint) "checkpoint " tacticSeq : tactic

13
stage0/src/Init/NotationExtra.lean generated
View file

@ -154,6 +154,19 @@ macro "calc " steps:withPosition(calcStep+) : tactic => `(exact calc $(steps.get
| `($(_) fun $x:ident => $p) => `({ $x // $p })
| _ => throw ()
/--
Apply function extensionality and introduce new hypotheses.
The tactic `funext` will keep applying new the `funext` lemma until the goal target is not reducible to
```
|- ((fun x => ...) = (fun x => ...))
```
The variant `funext h₁ ... hₙ` applies `funext` `n` times, and uses the given identifiers to name the new hypotheses.
Patterns can be used like in the `intro` tactic. Example, given a goal
```
|- ((fun x : Nat × Bool => ...) = (fun x => ...))
```
`funext (a, b)` applies `funext` once and performs pattern matching on the newly introduced pair.
-/
syntax "funext " (colGt term:max)+ : tactic
macro_rules

17
stage0/src/Init/SizeOf.lean generated
View file

@ -60,14 +60,25 @@ deriving instance SizeOf for EStateM.Result
@[simp] theorem Unit.sizeOf (u : Unit) : sizeOf u = 1 := rfl
@[simp] theorem Bool.sizeOf_eq_one (b : Bool) : sizeOf b = 1 := by cases b <;> rfl
namespace Lean
/- We manually define `Lean.Name` instance because we use
an opaque function for computing the hashcode field. -/
protected noncomputable def Lean.Name.sizeOf : Name → Nat
protected noncomputable def Name.sizeOf : Name → Nat
| anonymous => 1
| str p s _ => 1 + Name.sizeOf p + sizeOf s
| num p n _ => 1 + Name.sizeOf p + sizeOf n
noncomputable instance : SizeOf Lean.Name where
noncomputable instance : SizeOf Name where
sizeOf n := n.sizeOf
deriving instance SizeOf for Lean.Syntax
@[simp] theorem Name.anonymous.sizeOf_spec : sizeOf anonymous = 1 :=
rfl
@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) (h : UInt64) : sizeOf (str p s h) = 1 + sizeOf p + sizeOf s :=
rfl
@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) (h : UInt64) : sizeOf (num p n h) = 1 + sizeOf p + sizeOf n :=
rfl
deriving instance SizeOf for Syntax
end Lean

4
stage0/src/Lean/Elab/App.lean generated
View file

@ -866,9 +866,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
let some expectedType := expectedType?
| throwError "invalid dotted identifier notation, expected type must be known"
forallTelescopeReducing expectedType fun _ resultType => do
let resultTypeFn := (← instantiateMVars resultType).getAppFn
let resultTypeFn := (← instantiateMVars resultType).consumeMData.getAppFn
tryPostponeIfMVar resultTypeFn
let .const declName .. := resultTypeFn
let .const declName .. := resultTypeFn.consumeMData
| throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
let idNew := declName ++ id.getId.eraseMacroScopes
unless (← getEnv).contains idNew do

2
stage0/src/Lean/Elab/DefView.lean generated
View file

@ -127,7 +127,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
let val ← match stx[3].getOptional? with
| some val => pure val
| none =>
let val ← `(default_or_ofNonempty%)
let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
pure <| mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
return {
ref := stx, kind := DefKind.opaque, modifiers := modifiers,

7
stage0/src/Lean/Elab/Extra.lean generated
View file

@ -350,7 +350,12 @@ def elabDefaultOrNonempty : TermElab := fun stx expectedType? => do
catch ex => try
mkOfNonempty expectedType
catch _ =>
throw ex
if stx[1].isNone then
throw ex
else
-- It is in the context of an `unsafe` constant. We can use sorry instead.
-- Another option is to make a recursive application since it is unsafe.
mkSorry expectedType false
builtin_initialize
registerTraceClass `Elab.binop

253
stage0/src/Lean/Elab/Inductive.lean generated
View file

@ -145,8 +145,8 @@ private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : O
match firstType? with
| none => pure type
| some firstType =>
withRef r.view.ref $ checkParamsAndResultType type firstType numParams
pure firstType
withRef r.view.ref <| checkParamsAndResultType type firstType numParams
return firstType
-- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) (i : Nat) (firstType? : Option Expr) : TermElabM Unit := do
@ -173,7 +173,7 @@ private partial def withInductiveLocalDecls {α} (rs : Array ElabHeaderResult) (
pure (r.view.shortDeclName, type)
let r0 := rs[0]
let params := r0.params
withLCtx r0.lctx r0.localInsts $ withRef r0.view.ref do
withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
let rec loop (i : Nat) (indFVars : Array Expr) := do
if h : i < namesAndTypes.size then
let (id, type) := namesAndTypes.get ⟨i, h⟩
@ -187,6 +187,86 @@ private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Boo
forallTelescopeReducing indFVarType fun xs _ =>
return xs.size > numParams
private def getArrowBinderNames (type : Expr) : Array Name :=
go type #[]
where
go (type : Expr) (acc : Array Name) : Array Name :=
match type with
| .forallE n _ b _ => go b (acc.push n)
| .mdata _ b _ => go b acc
| _ => acc
/--
Replace binder names in `type` with `newNames`.
Remark: we only replace the names for binder containing macroscopes.
-/
private def replaceArrowBinderNames (type : Expr) (newNames : Array Name) : Expr :=
go type 0
where
go (type : Expr) (i : Nat) : Expr :=
if i < newNames.size then
match type with
| .forallE n d b data =>
if n.hasMacroScopes then
mkForall newNames[i] data.binderInfo d (go b (i+1))
else
mkForall n data.binderInfo d (go b (i+1))
| _ => type
else
type
/--
Reorder contructor arguments to improve the effectiveness of the `fixedIndicesToParams` method.
The idea is quite simple. Given a constructor type of the form
```
(a₁ : A₁) → ... → (aₙ : Aₙ) → C b₁ ... bₘ
```
We try to find the longest prefix `b₁ ... bᵢ`, `i ≤ m` s.t.
- each `bₖ` is in `{a₁, ..., aₙ}`
- each `bₖ` only depends on variables in `{b₁, ..., bₖ₋₁}`
Then, it moves this prefix `b₁ ... bᵢ` to the front.
-/
private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
forallTelescopeReducing ctorType fun as type => do
/- `type` is of the form `C ...` where `C` is the inductive datatype being defined. -/
let bs := type.getAppArgs
let mut as := as
let mut bsPrefix := #[]
for b in bs do
unless b.isFVar && as.contains b do
break
let localDecl ← getFVarLocalDecl b
if (← localDeclDependsOnPred localDecl fun fvarId => as.any fun p => p.fvarId! == fvarId) then
break
bsPrefix := bsPrefix.push b
as := as.erase b
if bsPrefix.isEmpty then
return ctorType
else
let r ← mkForallFVars (bsPrefix ++ as) type
/- `r` already contains the resulting type.
To be able to produce more better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
This is important when some of contructor parameters were inferred using the auto-bound implicit feature.
For example, in the following declaration.
```
inductive Member : α → List α → Type u
| head : Member a (a::as)
| tail : Member a bs → Member a (b::bs)
```
if we do not copy the binder names
```
#check @Member.head
```
produces `@Member.head : {x : Type u_1} → {a : x} → {as : List x} → Member a (a :: as)`
which is correct, but a bit confusing. By copying the binder names, we obtain
`@Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)`
-/
let C := type.getAppFn
let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C))
return replaceArrowBinderNames r binderNames[:bsPrefix.size]
/-
Elaborate constructor types.
@ -223,6 +303,7 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
let type ← mkForallFVars ctorParams type
let extraCtorParams ← Term.collectUnassignedMVars type
let type ← mkForallFVars extraCtorParams type
let type ← reorderCtorArgs type
let type ← mkForallFVars params type
return { name := ctorView.declName, type }
where
@ -278,58 +359,11 @@ def shouldInferResultUniverse (u : Level) : TermElabM Bool := do
match u.getLevelOffset with
| Level.mvar mvarId _ => do
Term.assignLevelMVar mvarId tmpIndParam
pure true
return true
| _ =>
throwError "cannot infer resulting universe level of inductive datatype, given level contains metavariables {mkSort u}, provide universe explicitly"
else
pure false
/-
Auxiliary function for `updateResultingUniverse`
`accLevelAtCtor u r rOffset us` add `u` components to `us` if they are not already there and it is different from the resulting universe level `r+rOffset`.
If `u` is a `max`, then its components are recursively processed.
If `u` is a `succ` and `rOffset > 0`, we process the `u`s child using `rOffset-1`.
This method is used to infer the resulting universe level of an inductive datatype. -/
def accLevelAtCtor : Level → Level → Nat → Array Level → TermElabM (Array Level)
| Level.max u v _, r, rOffset, us => do let us ← accLevelAtCtor u r rOffset us; accLevelAtCtor v r rOffset us
| Level.imax u v _, r, rOffset, us => do let us ← accLevelAtCtor u r rOffset us; accLevelAtCtor v r rOffset us
| Level.zero _, _, _, us => pure us
| Level.succ u _, r, rOffset+1, us => accLevelAtCtor u r rOffset us
| u, r, rOffset, us =>
if rOffset == 0 && u == r then pure us
else if r.occurs u then throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
else if rOffset > 0 then throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
else if us.contains u then pure us
else pure (us.push u)
/- Auxiliary function for `updateResultingUniverse` -/
private partial def collectUniversesFromCtorTypeAux (r : Level) (rOffset : Nat) : Nat → Expr → Array Level → TermElabM (Array Level)
| 0, Expr.forallE n d b c, us => do
let u ← getLevel d
let u ← instantiateLevelMVars u
let us ← accLevelAtCtor u r rOffset us
withLocalDecl n c.binderInfo d fun x =>
let e := b.instantiate1 x
collectUniversesFromCtorTypeAux r rOffset 0 e us
| i+1, Expr.forallE n d b c, us => do
withLocalDecl n c.binderInfo d fun x =>
let e := b.instantiate1 x
collectUniversesFromCtorTypeAux r rOffset i e us
| _, _, us => pure us
/- Auxiliary function for `updateResultingUniverse` -/
private partial def collectUniversesFromCtorType
(r : Level) (rOffset : Nat) (ctorType : Expr) (numParams : Nat) (us : Array Level) : TermElabM (Array Level) :=
collectUniversesFromCtorTypeAux r rOffset numParams ctorType us
/- Auxiliary function for `updateResultingUniverse` -/
private partial def collectUniverses (r : Level) (rOffset : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (Array Level) := do
let mut us := #[]
for indType in indTypes do
for ctor in indType.ctors do
us ← collectUniversesFromCtorType r rOffset ctor.type numParams us
return us
return false
def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level :=
if us.isEmpty && rOffset == 0 then
@ -337,10 +371,51 @@ def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level :=
else
let r := Level.mkNaryMax us.toList
if rOffset == 0 && !r.isZero && !r.isNeverZero then
(mkLevelMax r levelOne).normalize
mkLevelMax r levelOne |>.normalize
else
r.normalize
/--
Auxiliary function for `updateResultingUniverse`
`accLevelAtCtor u r rOffset` add `u` to state if it is not already there and
it is different from the resulting universe level `r+rOffset`.
If `u` is a `max`, then its components are recursively processed.
If `u` is a `succ` and `rOffset > 0`, we process the `u`s child using `rOffset-1`.
This method is used to infer the resulting universe level of an inductive datatype.
-/
def accLevelAtCtor (u : Level) (r : Level) (rOffset : Nat) : StateRefT (Array Level) TermElabM Unit := do
match u, rOffset with
| Level.max u v _, rOffset => accLevelAtCtor u r rOffset; accLevelAtCtor v r rOffset
| Level.imax u v _, rOffset => accLevelAtCtor u r rOffset; accLevelAtCtor v r rOffset
| Level.zero _, _ => return ()
| Level.succ u _, rOffset+1 => accLevelAtCtor u r rOffset
| u, rOffset =>
if rOffset == 0 && u == r then
return ()
else if r.occurs u then
throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
else if rOffset > 0 then
throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
else if (← get).contains u then
return ()
else
modify fun us => us.push u
/-- Auxiliary function for `updateResultingUniverse` -/
private partial def collectUniverses (r : Level) (rOffset : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (Array Level) := do
let (_, us) ← go |>.run #[]
return us
where
go : StateRefT (Array Level) TermElabM Unit :=
indTypes.forM fun indType => indType.ctors.forM fun ctor =>
forallTelescopeReducing ctor.type fun ctorParams _ =>
for ctorParam in ctorParams[numParams:] do
let type ← inferType ctorParam
let u ← instantiateLevelMVars (← getLevel type)
accLevelAtCtor u r rOffset
private def updateResultingUniverse (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do
let r ← getResultingUniverse indTypes
let rOffset : Nat := r.getOffset
@ -368,8 +443,56 @@ def checkResultingUniverse (u : Level) : TermElabM Unit := do
if !u.isZero && !u.isNeverZero then
throwError "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'{indentD u}"
private def checkResultingUniverses (indTypes : List InductiveType) : TermElabM Unit := do
checkResultingUniverse (← getResultingUniverse indTypes)
/--
Execute `k` using the `Syntax` reference associated with constructor `ctorName`.
-/
def withCtorRef (views : Array InductiveView) (ctorName : Name) (k : TermElabM α) : TermElabM α := do
for view in views do
for ctorView in view.ctors do
if ctorView.declName == ctorName then
return (← withRef ctorView.ref k)
k
private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize
checkResultingUniverse u
unless u.isZero do
indTypes.forM fun indType => indType.ctors.forM fun ctor =>
forallTelescopeReducing ctor.type fun ctorArgs type => do
for ctorArg in ctorArgs[numParams:] do
let type ← inferType ctorArg
let v := (← instantiateLevelMVars (← getLevel type)).normalize
let rec check (v' : Level) (u' : Level) : TermElabM Unit :=
match v', u' with
| .succ v' _, .succ u' _ => check v' u'
| .mvar id _, .param .. =>
/- Special case:
The constructor parameter `v` is at unverse level `?v+k` and
the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
Thus, `?v := u'` is the only choice for satisfying the universe contraint `?v+k <= u'+k`.
Note that, we still generate an error for cases where there is more than one of satisfying the constraint.
Examples:
-----------------------------------------------------------
| ctor universe level | inductive datatype universe level |
-----------------------------------------------------------
| ?v | max u w |
-----------------------------------------------------------
| ?v | u + 1 |
-----------------------------------------------------------
-/
assignLevelMVar id u'
| .mvar id _, .zero _ => assignLevelMVar id u' -- TODO: merge with previous case
| _, _ =>
unless u.geq v do
let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
let localDecl ← getFVarLocalDecl ctorArg
unless localDecl.userName.hasMacroScopes do
msg := msg ++ m!" '{ctorArg}'"
msg := msg ++ m!" has type{indentExpr type}"
msg := msg ++ m!"\nat universe level{indentD v}"
msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
withCtorRef views ctor.name <| throwError msg
check v u
private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
indTypes.forM fun indType => do
@ -383,15 +506,15 @@ private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : T
private def withUsed {α} (vars : Array Expr) (indTypes : List InductiveType) (k : Array Expr → TermElabM α) : TermElabM α := do
let (lctx, localInsts, vars) ← removeUnused vars indTypes
withLCtx lctx localInsts $ k vars
withLCtx lctx localInsts <| k vars
private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
indTypes.mapM fun indType => do
let type ← mkForallFVars vars indType.type
let ctors ← indType.ctors.mapM fun ctor => do
let ctorType ← mkForallFVars vars ctor.type
pure { ctor with type := ctorType }
pure { indType with type := type, ctors := ctors }
return { ctor with type := ctorType }
return { indType with type := type, ctors := ctors }
private def collectLevelParamsInInductive (indTypes : List InductiveType) : Array Name := Id.run <| do
let mut usedParams : CollectLevelParams.State := {}
@ -425,8 +548,8 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars :
| none => none
| some c => mkAppN c (params.extract 0 numVars)
mkForallFVars params type
pure { ctor with type := type }
pure { indType with ctors := ctors }
return { ctor with type := type }
return { indType with ctors := ctors }
abbrev Ctor2InferMod := Std.HashMap Name Bool
@ -512,7 +635,6 @@ private def isDomainDefEq (arrowType : Expr) (type : Expr) : MetaM Bool := do
/--
Convert fixed indices to parameters.
TODO: we currently only convert a prefix of the indices, and we do not try to reorder binders.
-/
private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM (Nat × List InductiveType) := do
let masks ← indTypes.mapM (computeFixedIndexBitMask numParams · indFVars)
@ -560,15 +682,18 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
indTypesArray := indTypesArray.push { name := r.view.declName, type := type, ctors := ctors : InductiveType }
Term.synthesizeSyntheticMVarsNoPostponing
let (numExplicitParams, indTypes) ← fixedIndicesToParams params.size indTypesArray indFVars
trace[Meta.debug] "numExplicitParams: {numExplicitParams}"
let u ← getResultingUniverse indTypes
let inferLevel ← shouldInferResultUniverse u
withUsed vars indTypes fun vars => do
let numVars := vars.size
let numParams := numVars + numExplicitParams
let indTypes ← updateParams vars indTypes
let indTypes ← levelMVarToParam indTypes
let indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else checkResultingUniverses indTypes; pure indTypes
let indTypes ←
if inferLevel then
updateResultingUniverse numParams (← levelMVarToParam indTypes)
else
checkResultingUniverses views numParams indTypes
levelMVarToParam indTypes
let usedLevelNames := collectLevelParamsInInductive indTypes
match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
| Except.error msg => throwError msg

14
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -623,11 +623,15 @@ private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fie
(levelMVarToParamAux scopeVars params fieldInfos).run' 1
private partial def collectUniversesFromFields (r : Level) (rOffset : Nat) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Level) := do
fieldInfos.foldlM (init := #[]) fun (us : Array Level) (info : StructFieldInfo) => do
let type ← inferType info.fvar
let u ← getLevel type
let u ← instantiateLevelMVars u
accLevelAtCtor u r rOffset us
let (_, us) ← go |>.run #[]
return us
where
go : StateRefT (Array Level) TermElabM Unit :=
for info in fieldInfos do
let type ← inferType info.fvar
let u ← getLevel type
let u ← instantiateLevelMVars u
accLevelAtCtor u r rOffset
private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : Expr) : TermElabM Expr := do
let r ← getResultUniverse type

50
stage0/src/Lean/Elab/Tactic/BuiltinTactic.lean generated
View file

@ -248,28 +248,38 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
assignExprMVar mvarId mvarNew
return mvarNew.mvarId!
@[builtinTactic «case»] def evalCase : Tactic
| stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
let gs ← getUnsolvedGoals
let g ←
if tag.isIdent then
let tag := tag.getId
let some g ← findTag? gs tag | throwError "tag not found"
pure g
else
getMainGoal
let gs := gs.erase g
let g ← renameInaccessibles g hs
setGoals [g]
let savedTag ← getMVarTag g
setMVarTag g Name.anonymous
try
private def evalCaseCore (stx : Syntax) (tag : Syntax) (hs : Array Syntax) (arr : Syntax) (tac : Syntax)
(closeOnFailure : Bool) : TacticM Unit := do
let gs ← getUnsolvedGoals
let g ←
if tag.isIdent then
let tag := tag.getId
let some g ← findTag? gs tag | throwError "tag not found"
pure g
else
getMainGoal
let gs := gs.erase g
let g ← renameInaccessibles g hs
setGoals [g]
let savedTag ← getMVarTag g
setMVarTag g Name.anonymous
try
if closeOnFailure then
withCaseRef arr tac do
closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
finally
setMVarTag g savedTag
done
setGoals gs
else
evalTactic tac
finally
setMVarTag g savedTag
done
setGoals gs
@[builtinTactic «case»] def evalCase : Tactic
| stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => evalCaseCore stx tag hs arr tac (closeOnFailure := true)
| _ => throwUnsupportedSyntax
@[builtinTactic «case'»] def evalCase' : Tactic
| stx@`(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => evalCaseCore stx tag hs arr tac (closeOnFailure := false)
| _ => throwUnsupportedSyntax
@[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic

18
stage0/src/Lean/Level.lean generated
View file

@ -553,6 +553,24 @@ def mkNaryMax : List Level → Level
| none => u
| u => u
def geq (u v : Level) : Bool :=
go u.normalize v.normalize
where
go (u v : Level) : Bool :=
u == v ||
match u, v with
| u, zero _ => true
| u, max v₁ v₂ _ => go u v₁ && go u v₂
| max u₁ u₂ _, v => go u₁ v || go u₂ v
| u, imax v₁ v₂ _ => go u v₁ && go u v₂
| imax u₁ u₂ _, v => go u₂ v
| succ u _, succ v _ => go u v
| _, _ =>
let v' := v.getLevelOffset
(u.getLevelOffset == v' || v'.isZero)
&& u.getOffset ≥ v.getOffset
termination_by _ u v => (u, v)
end Level
open Std (HashMap HashSet PHashMap PHashSet)

57
stage0/src/Lean/Meta/PPGoal.lean generated
View file

@ -34,7 +34,12 @@ structure State where
modified : Bool := false
structure Context where
goalTarget : Expr
/--
If true we make a declaration "visible" if it has visible backward dependencies.
Remark: recall that for the `Prop` case, the declaration is moved to `hiddenInaccessibleProp`
-/
backwardDeps : Bool
goalTarget : Expr
abbrev M := ReaderT Context $ StateRefT State MetaM
@ -95,17 +100,17 @@ def fixpointStep : M Unit := do
(← getLCtx).forM fun localDecl => do
let fvarId := localDecl.fvarId
if (← get).hiddenInaccessible.contains fvarId then
if (← hasVisibleDep localDecl) then
/- localDecl is marked to be hidden, but it has a (backward) visible dependency. -/
unmark fvarId
if (← isProp localDecl.type) then
unless (← hasInaccessibleNameDep localDecl) do
moveToHiddeProp fvarId
if (← read).backwardDeps then
if (← hasVisibleDep localDecl) then
/- localDecl is marked to be hidden, but it has a (backward) visible dependency. -/
unmark fvarId
if (← isProp localDecl.type) then
unless (← hasInaccessibleNameDep localDecl) do
moveToHiddeProp fvarId
else
visitVisibleExpr localDecl.type
match localDecl.value? with
| some value => visitVisibleExpr value
| _ => pure ()
let some value := localDecl.value? | return ()
visitVisibleExpr value
partial def fixpoint : M Unit := do
modify fun s => { s with modified := false }
@ -113,6 +118,16 @@ partial def fixpoint : M Unit := do
if (← get).modified then
fixpoint
/--
Construct initial `FVarIdSet` containting free variables ids that have inaccessible user names.
-/
private def getInitialHiddenInaccessible (propOnly : Bool) : MetaM FVarIdSet := do
(← getLCtx).foldlM (init := {}) fun r localDecl => do
if localDecl.userName.isInaccessibleUserName then
if (← pure !propOnly <||> isProp localDecl.type) then
return r.insert localDecl.fvarId
return r
/-
If pp.inaccessibleNames == false, then collect two sets of `FVarId`s : `hiddenInaccessible` and `hiddenInaccessibleProp`
1- `hiddenInaccessible` contains `FVarId`s of free variables with inaccessible names that
@ -123,19 +138,23 @@ Both sets do not contain `FVarId`s that contain visible backward or forward depe
The `goalTarget` counts as a forward dependency.
We say a name is visible if it is a free variable with FVarId not in `hiddenInaccessible` nor `hiddenInaccessibleProp`
For propositions in `hiddenInaccessibleProp`, we show only their types when displaying a goal.
Remark: when `pp.inaccessibleNames == true`, we still compute `hiddenInaccessibleProp` to prevent the
goal from being littered with irrelevant names.
-/
def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do
let lctx ← getLCtx
if pp.inaccessibleNames.get (← getOptions) then
/- Don't hide inaccessible names when `pp.inaccessibleNames` is set to true. -/
return ({}, {})
-- If `pp.inaccessibleNames == true`, we still must compute `hiddenInaccessibleProp`.
let hiddenInaccessible ← getInitialHiddenInaccessible (propOnly := true)
let (_, s) ← fixpoint.run { backwardDeps := false, goalTarget } |>.run { hiddenInaccessible }
return ({}, s.hiddenInaccessible)
else
let lctx ← getLCtx
let hiddenInaccessible := lctx.foldl (init := {}) fun hiddenInaccessible localDecl => Id.run <| do
if localDecl.userName.isInaccessibleUserName then
hiddenInaccessible.insert localDecl.fvarId
else
hiddenInaccessible
let (_, s) ← fixpoint.run { goalTarget := goalTarget } |>.run { hiddenInaccessible := hiddenInaccessible }
let hiddenInaccessible ← getInitialHiddenInaccessible (propOnly := false)
let (_, s) ← fixpoint.run { backwardDeps := true, goalTarget } |>.run { hiddenInaccessible }
return (s.hiddenInaccessible, s.hiddenInaccessibleProp)
end ToHide

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

@ -245,7 +245,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def waitIfTypeContainsMVar := leading_parser "wait_if_type_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtinTermParser] def waitIfContainsMVar := leading_parser "wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
@[builtinTermParser] def defaultOrOfNonempty := leading_parser "default_or_ofNonempty%"
@[builtinTermParser] def defaultOrOfNonempty := leading_parser "default_or_ofNonempty% " >> optional "unsafe"
def namedArgument := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := leading_parser ".."

8
stage0/src/Lean/Widget/InteractiveGoal.lean generated
View file

@ -87,15 +87,15 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
withLCtx lctx mvarDecl.localInstances do
let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
-- The following two `let rec`s are being used to control the generated code size.
-- Then should be remove after we rewrite the compiler in Lean
-- They should be removed after we rewrite the compiler in Lean
let rec pushPending (ids : Array Name) (type? : Option Expr) (hyps : Array InteractiveHypothesis)
: MetaM (Array InteractiveHypothesis) :=
if ids.isEmpty then
pure hyps
else
match ids, type? with
| _, none => pure hyps
| _, some type => addInteractiveHypothesis hyps ids type
match type? with
| none => pure hyps
| some type => addInteractiveHypothesis hyps ids type
let rec ppVars (varNames : Array Name) (prevType? : Option Expr) (hyps : Array InteractiveHypothesis) (localDecl : LocalDecl)
: MetaM (Array Name × Option Expr × Array InteractiveHypothesis) := do
if hiddenProp.contains localDecl.fvarId then

2
stage0/src/stdlib_flags.h generated
View file

@ -8,7 +8,7 @@ options get_default_options() {
// switch to `true` for ABI-breaking changes affecting meta code
opts = opts.update({"interpreter", "prefer_native"}, false);
// switch to `true` for changing built-in parsers used in quotations
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
#endif
return opts;
}

1528
stage0/stdlib/Init/Classical.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Init/Data/Array/Basic.c generated
View file

@ -8853,7 +8853,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_Array_swapAt_x21___rarg___closed__3;
x_2 = l_Array_insertAt___rarg___closed__1;
x_3 = lean_unsigned_to_nat(701u);
x_3 = lean_unsigned_to_nat(703u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Array_insertAt___rarg___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

1439
stage0/stdlib/Init/Data/Array/Mem.c generated
View file

File diff suppressed because it is too large Load diff

1781
stage0/stdlib/Init/Data/List/BasicAux.c generated
View file

File diff suppressed because it is too large Load diff

195
stage0/stdlib/Init/Data/Range.c generated
View file

@ -34,12 +34,14 @@ static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__9;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x5d__1___closed__3;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__7;
static lean_object* l_Std_Range_term_x5b___x3a___x5d___closed__7;
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_term_x5b_x3a___x3a___x5d;
LEAN_EXPORT lean_object* l_Std_Range_step___default;
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(lean_object*, lean_object*);
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__16;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__24;
lean_object* lean_array_push(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_instMembershipNatRange;
LEAN_EXPORT lean_object* l_Std_Range_instForInRangeNat___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__29;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x5d__1___closed__1;
@ -51,6 +53,7 @@ static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__R
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__2;
LEAN_EXPORT lean_object* l_Std_Range_forM_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__13;
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x5d__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__11;
@ -86,11 +89,13 @@ static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__3;
LEAN_EXPORT lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x3a___x5d__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__15;
static lean_object* l_Std_Range_term_x5b___x3a___x5d___closed__4;
LEAN_EXPORT lean_object* l_Std_Range_instForIn_x27RangeNatInferInstanceMembershipInstMembershipNatRange(lean_object*, lean_object*);
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__18;
static lean_object* l_Std_Range_term_x5b___x3a___x5d___closed__5;
LEAN_EXPORT lean_object* l_Std_Range_start___default;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__37;
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__14;
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__6;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__27;
@ -120,6 +125,7 @@ static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__R
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__28;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__14;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__22;
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop(lean_object*, lean_object*);
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__33;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__15;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__30;
@ -127,6 +133,7 @@ static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__R
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__13;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__41;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__3;
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x3a___x5d__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_term_x5b_x3a___x5d;
@ -140,16 +147,19 @@ static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__12;
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__7;
static lean_object* l_Std_Range_term_x5b___x3a___x5d___closed__6;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x5d__1___closed__5;
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__12;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x3a___x5d__1___closed__2;
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__16;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b_x3a___x5d__1___closed__26;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x5d__1___closed__10;
LEAN_EXPORT lean_object* l_Std_Range_instForIn_x27RangeNatInferInstanceMembershipInstMembershipNatRange___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_term_x5b___x3a___x5d___closed__3;
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__20;
static lean_object* l_Std_Range_term_x5b_x3a___x5d___closed__10;
static lean_object* l_Std_Range___aux__Init__Data__Range______macroRules__Std__Range__term_x5b___x3a___x3a___x5d__1___closed__6;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static lean_object* _init_l_Std_Range_start___default() {
_start:
{
@ -166,6 +176,14 @@ x_1 = lean_unsigned_to_nat(1u);
return x_1;
}
}
static lean_object* _init_l_Std_instMembershipNatRange() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___rarg___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) {
_start:
{
@ -335,6 +353,181 @@ x_3 = lean_alloc_closure((void*)(l_Std_Range_instForInRangeNat___rarg), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg___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) {
_start:
{
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
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_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
lean_dec(x_8);
x_10 = lean_ctor_get(x_1, 0);
lean_inc(x_10);
lean_dec(x_1);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_apply_2(x_11, lean_box(0), x_9);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_8, 0);
lean_inc(x_13);
lean_dec(x_8);
x_14 = lean_nat_add(x_2, x_3);
lean_dec(x_2);
x_15 = l_Std_Range_forIn_x27_loop___rarg(x_1, x_4, x_5, x_3, x_6, x_7, x_14, lean_box(0), x_13);
lean_dec(x_7);
return x_15;
}
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg(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:
{
uint8_t x_10;
x_10 = lean_nat_dec_lt(x_7, x_3);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_apply_2(x_12, lean_box(0), x_9);
return x_13;
}
else
{
lean_object* x_14; uint8_t x_15;
x_14 = lean_unsigned_to_nat(0u);
x_15 = lean_nat_dec_eq(x_6, x_14);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_16 = lean_unsigned_to_nat(1u);
x_17 = lean_nat_sub(x_6, x_16);
x_18 = lean_ctor_get(x_1, 1);
lean_inc(x_18);
lean_inc(x_5);
lean_inc(x_7);
x_19 = lean_apply_3(x_5, x_7, lean_box(0), x_9);
x_20 = lean_alloc_closure((void*)(l_Std_Range_forIn_x27_loop___rarg___lambda__1), 8, 7);
lean_closure_set(x_20, 0, x_1);
lean_closure_set(x_20, 1, x_7);
lean_closure_set(x_20, 2, x_4);
lean_closure_set(x_20, 3, x_2);
lean_closure_set(x_20, 4, x_3);
lean_closure_set(x_20, 5, x_5);
lean_closure_set(x_20, 6, x_17);
x_21 = lean_apply_4(x_18, lean_box(0), lean_box(0), x_19, x_20);
return x_21;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_22 = lean_ctor_get(x_1, 0);
lean_inc(x_22);
lean_dec(x_1);
x_23 = lean_ctor_get(x_22, 1);
lean_inc(x_23);
lean_dec(x_22);
x_24 = lean_apply_2(x_23, lean_box(0), x_9);
return x_24;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_Range_forIn_x27_loop___rarg___boxed), 9, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___rarg___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_Std_Range_forIn_x27_loop___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_6);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_7 = lean_ctor_get(x_2, 2);
lean_inc(x_7);
lean_dec(x_2);
lean_inc(x_6);
lean_inc(x_5);
x_8 = l_Std_Range_forIn_x27_loop___rarg(x_1, x_5, x_6, x_7, x_4, x_6, x_5, lean_box(0), x_3);
lean_dec(x_6);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forIn_x27(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_Range_forIn_x27___rarg), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Range_instForIn_x27RangeNatInferInstanceMembershipInstMembershipNatRange___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_7 = lean_ctor_get(x_2, 2);
lean_inc(x_7);
lean_dec(x_2);
lean_inc(x_6);
lean_inc(x_5);
x_8 = l_Std_Range_forIn_x27_loop___rarg(x_1, x_5, x_6, x_7, x_4, x_6, x_5, lean_box(0), x_3);
lean_dec(x_6);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Std_Range_instForIn_x27RangeNatInferInstanceMembershipInstMembershipNatRange(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_Range_instForIn_x27RangeNatInferInstanceMembershipInstMembershipNatRange___rarg), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Range_forM_loop___rarg___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) {
_start:
{
@ -2874,6 +3067,8 @@ l_Std_Range_start___default = _init_l_Std_Range_start___default();
lean_mark_persistent(l_Std_Range_start___default);
l_Std_Range_step___default = _init_l_Std_Range_step___default();
lean_mark_persistent(l_Std_Range_step___default);
l_Std_instMembershipNatRange = _init_l_Std_instMembershipNatRange();
lean_mark_persistent(l_Std_instMembershipNatRange);
l_Std_Range_instForMRangeNat___closed__1 = _init_l_Std_Range_instForMRangeNat___closed__1();
lean_mark_persistent(l_Std_Range_instForMRangeNat___closed__1);
l_Std_Range_term_x5b_x3a___x5d___closed__1 = _init_l_Std_Range_term_x5b_x3a___x5d___closed__1();

410
stage0/stdlib/Init/Notation.c generated
View file

@ -63,6 +63,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_fail;
static lean_object* l___aux__Init__Notation______macroRules__term___x5e____1___closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_first;
static lean_object* l_Lean_Parser_Tactic_withUnfoldingAll___closed__6;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__7;
static lean_object* l_Lean_Parser_Tactic_letrec___closed__12;
static lean_object* l___aux__Init__Notation______macroRules__term___x2b____1___closed__4;
static lean_object* l_Lean_Parser_Tactic_revert___closed__2;
@ -283,6 +284,7 @@ static lean_object* l_Lean_Parser_Tactic_location___closed__3;
static lean_object* l_Lean_Parser_Tactic_refine_x27___closed__6;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3c_x3c____1___closed__9;
static lean_object* l_Lean_Parser_Tactic_fail___closed__7;
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__2;
static lean_object* l_prioLow___closed__3;
static lean_object* l_Lean_Parser_Tactic_clear___closed__6;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2264____2(lean_object*, lean_object*, lean_object*);
@ -371,6 +373,7 @@ LEAN_EXPORT lean_object* l_Lean___aux__Init__Notation______macroRules__term_x5b_
static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__24;
static lean_object* l_Lean_Parser_Tactic_tacticLet_____closed__4;
static lean_object* l_Lean_Parser_Tactic_rwRule___closed__8;
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__1;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__8;
static lean_object* l_term_x7b_____x3a___x2f_x2f___x7d___closed__16;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3d____1___closed__6;
@ -441,6 +444,7 @@ static lean_object* l_term___u2228_____closed__6;
static lean_object* l_term___x5e_____closed__3;
LEAN_EXPORT lean_object* l_term_x7e_x7e_x7e__;
LEAN_EXPORT lean_object* l_term___x3c__;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_case_x27;
static lean_object* l___aux__Init__Notation______unexpand__Function__comp__1___closed__2;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRfl_x27__1___closed__5;
static lean_object* l_Lean_Parser_Tactic_rotateRight___closed__1;
@ -573,6 +577,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__Complement__comp
static lean_object* l_term___x3c_x7c_x3e_____closed__2;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x26_x26____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_stx___x2c_x2a_x2c_x3f___closed__3;
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__precLead__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_term___x2f_____closed__1;
static lean_object* l_stx___x2c_x2a___closed__1;
@ -589,6 +594,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticRefine__lift_x27_____closed__5;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_induction;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticInfer__instance__1___closed__3;
static lean_object* l_Lean_Parser_Tactic_induction___closed__19;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__6;
static lean_object* l_Lean_Parser_Tactic_rwWithRfl___closed__3;
static lean_object* l_Lean_Parser_Tactic_letrec___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x26_x26_x26____1___closed__7;
@ -614,6 +620,7 @@ LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term_u2039___u
static lean_object* l_termIfLet___x3a_x3d__Then__Else_____closed__18;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3d____2(lean_object*, lean_object*, lean_object*);
static lean_object* l_term_x21_____closed__5;
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__3;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTrivial__4___closed__2;
static lean_object* l_Lean_Parser_Tactic_generalizeArg___closed__2;
static lean_object* l_Lean_Parser_Tactic_withReducible___closed__4;
@ -637,6 +644,7 @@ LEAN_EXPORT lean_object* l_term___x3e__;
LEAN_EXPORT lean_object* l_termMax__prec;
static lean_object* l_Lean_Parser_Tactic_subst___closed__2;
static lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticStop____1(lean_object*, lean_object*, lean_object*);
static lean_object* l___aux__Init__Notation______macroRules__term___x3d_x3d____1___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_dbgTrace;
static lean_object* l_Lean_Parser_Tactic_focus___closed__4;
@ -851,6 +859,7 @@ static lean_object* l_Lean_Parser_Tactic_withReducibleAndInstances___closed__1;
static lean_object* l_stx___x3f___closed__3;
static lean_object* l_Lean_Parser_Tactic_checkpoint___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__10;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__5;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__letrec__1___closed__1;
static lean_object* l_Lean_Parser_Tactic_fail___closed__2;
static lean_object* l_Lean_Parser_Tactic_intro___closed__11;
@ -960,6 +969,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___xd7____1___c
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___x24______1(lean_object*, lean_object*, lean_object*);
static lean_object* l_prioHigh___closed__5;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x3c_x3c____1___closed__8;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x2f____1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c_x7c_x3e____1___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__prioDefault__1___closed__1;
@ -1068,6 +1078,7 @@ static lean_object* l_Lean_Parser_Tactic_simpLemma___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__term___x3c____1___closed__6;
static lean_object* l_term___x2d_____closed__3;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2228____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__2;
static lean_object* l_term___x3c_x24_x3e_____closed__4;
static lean_object* l_Lean_Parser_Tactic_withReducibleAndInstances___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__2;
@ -1142,6 +1153,7 @@ static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__
static lean_object* l_term_x25_x5b___x7c___x5d___closed__10;
static lean_object* l_term___x7c_x3e_____closed__3;
static lean_object* l_Lean_Parser_Tactic_intro___closed__7;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__9;
static lean_object* l___aux__Init__Notation______macroRules__term___x3e_x3e_x3e____1___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__3;
static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__15;
@ -1203,6 +1215,7 @@ extern lean_object* l_Lean_instInhabitedSyntax;
static lean_object* l_term___x3c_x2a_x3e_____closed__3;
static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__14;
static lean_object* l_Lean_Parser_Tactic_tacticLet_x27_____closed__5;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__8;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticHave_____x3a_x3d____1___closed__2;
static lean_object* l_term___x3d_x3d_____closed__5;
static lean_object* l_term_x2d_____closed__5;
@ -1219,6 +1232,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticShow_____closed__5;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__term___u2264____1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__termIfThenElse__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_termWithout__expected__type_____closed__5;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__1;
static lean_object* l_Lean_Parser_Tactic_withReducibleAndInstances___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___closed__2;
static lean_object* l_Lean_Parser_Syntax_addPrio___closed__6;
@ -1248,6 +1262,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_failIfSuccess;
static lean_object* l_Lean_Parser_Tactic_simpAll___closed__2;
static lean_object* l_Lean_Parser_Tactic_paren___closed__1;
static lean_object* l_stx___x2c_x2a___closed__5;
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__4;
static lean_object* l___aux__Init__Notation______macroRules__term___x25____1___closed__8;
static lean_object* l___aux__Init__Notation______macroRules__stx___x2b__1___closed__7;
static lean_object* l___aux__Init__Notation______macroRules__term___x3a_x3a____1___closed__1;
@ -1506,6 +1521,7 @@ static lean_object* l_stx___x3c_x7c_x3e_____closed__5;
static lean_object* l_term_u2039___u203a___closed__2;
static lean_object* l___aux__Init__Notation______macroRules__term___x2a_x3e____1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__4;
LEAN_EXPORT lean_object* l___aux__Init__Notation______macroRules__stx___x2c_x2b_x2c_x3f__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Notation______unexpand__HAppend__hAppend__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_first___closed__14;
@ -1818,6 +1834,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_renameI___closed__6;
static lean_object* l_term___u2208_____closed__5;
static lean_object* l_term_x7e_x7e_x7e_____closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticStop__;
static lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticHave____1___closed__1;
static lean_object* l___aux__Init__Notation______macroRules__termDepIfThenElse__1___closed__2;
static lean_object* l_Lean_Parser_Tactic_induction___closed__4;
@ -1976,6 +1993,7 @@ static lean_object* l___aux__Init__Notation______macroRules__term___x2a____1___c
static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__3;
static lean_object* l___aux__Init__Notation______macroRules__term___u2218____1___closed__3;
static lean_object* l_Lean_Parser_Tactic_tacticHave_x27_____closed__4;
static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__6;
LEAN_EXPORT lean_object* l_term___x5e__;
static lean_object* l_Lean_Parser_Tactic_intro___closed__14;
static lean_object* l_termIfThenElse___closed__8;
@ -31955,6 +31973,122 @@ x_1 = l_Lean_Parser_Tactic_case___closed__13;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("case'");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_intro___closed__2;
x_2 = l_Lean_Parser_Tactic_case_x27___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("case' ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_case_x27___closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(6, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_case_x27___closed__4;
x_3 = l_Lean_Parser_Tactic_intros___closed__6;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_case_x27___closed__5;
x_3 = l_Lean_Parser_Tactic_case___closed__6;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_case_x27___closed__6;
x_3 = l_Lean_Parser_Tactic_rename___closed__7;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_case_x27___closed__7;
x_3 = l_Lean_Parser_Tactic_case___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_case_x27___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_Parser_Tactic_case_x27___closed__8;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_case_x27() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_case_x27___closed__9;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__1() {
_start:
{
@ -43619,6 +43753,248 @@ x_1 = l_Lean_Parser_Tactic_dbgTrace___closed__6;
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("tacticStop_");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_intro___closed__2;
x_2 = l_Lean_Parser_Tactic_tacticStop_____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("stop");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticStop_____closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(6, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Syntax_addPrec___closed__10;
x_2 = l_Lean_Parser_Tactic_tacticStop_____closed__4;
x_3 = l_Lean_Parser_Tactic_case___closed__11;
x_4 = lean_alloc_ctor(2, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop_____closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticStop_____closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_Parser_Tactic_tacticStop_____closed__5;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_tacticStop__() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_tacticStop_____closed__6;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticStop____1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_tacticStop_____closed__2;
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; uint8_t x_9;
x_8 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
lean_object* x_10; 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; 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; 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; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_10 = lean_ctor_get(x_8, 0);
x_11 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRepeat____1___closed__1;
lean_inc(x_10);
x_12 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticAdmit__1___closed__1;
x_14 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_14, 0, x_10);
lean_ctor_set(x_14, 1, x_13);
x_15 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_16 = lean_array_push(x_15, x_14);
x_17 = lean_box(2);
x_18 = l_Lean_Parser_Tactic_tacticSorry___closed__2;
x_19 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_18);
lean_ctor_set(x_19, 2, x_16);
x_20 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
x_21 = lean_array_push(x_20, x_19);
x_22 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
x_23 = lean_array_push(x_21, x_22);
x_24 = l_Lean_Parser_Tactic_first___closed__8;
x_25 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_25, 0, x_17);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_25, 2, x_23);
x_26 = lean_array_push(x_15, x_25);
x_27 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_28 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_28, 0, x_17);
lean_ctor_set(x_28, 1, x_27);
lean_ctor_set(x_28, 2, x_26);
x_29 = lean_array_push(x_15, x_28);
x_30 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
x_31 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_31, 0, x_17);
lean_ctor_set(x_31, 1, x_30);
lean_ctor_set(x_31, 2, x_29);
x_32 = lean_array_push(x_15, x_31);
x_33 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
x_34 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_34, 0, x_17);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set(x_34, 2, x_32);
x_35 = lean_array_push(x_20, x_12);
x_36 = lean_array_push(x_35, x_34);
x_37 = l_Lean_Parser_Tactic_tacticRepeat_____closed__2;
x_38 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_38, 0, x_17);
lean_ctor_set(x_38, 1, x_37);
lean_ctor_set(x_38, 2, x_36);
x_39 = lean_array_push(x_15, x_38);
x_40 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_40, 0, x_17);
lean_ctor_set(x_40, 1, x_27);
lean_ctor_set(x_40, 2, x_39);
x_41 = lean_array_push(x_15, x_40);
x_42 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__2;
x_43 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_43, 0, x_17);
lean_ctor_set(x_43, 1, x_42);
lean_ctor_set(x_43, 2, x_41);
lean_ctor_set(x_8, 0, x_43);
return x_8;
}
else
{
lean_object* x_44; 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; 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; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79;
x_44 = lean_ctor_get(x_8, 0);
x_45 = lean_ctor_get(x_8, 1);
lean_inc(x_45);
lean_inc(x_44);
lean_dec(x_8);
x_46 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticRepeat____1___closed__1;
lean_inc(x_44);
x_47 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_47, 0, x_44);
lean_ctor_set(x_47, 1, x_46);
x_48 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticAdmit__1___closed__1;
x_49 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_49, 0, x_44);
lean_ctor_set(x_49, 1, x_48);
x_50 = l___aux__Init__Notation______macroRules__precMax__1___closed__4;
x_51 = lean_array_push(x_50, x_49);
x_52 = lean_box(2);
x_53 = l_Lean_Parser_Tactic_tacticSorry___closed__2;
x_54 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
lean_ctor_set(x_54, 2, x_51);
x_55 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__10;
x_56 = lean_array_push(x_55, x_54);
x_57 = l___aux__Init__Notation______macroRules__stx___x2c_x2a__1___closed__12;
x_58 = lean_array_push(x_56, x_57);
x_59 = l_Lean_Parser_Tactic_first___closed__8;
x_60 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_60, 0, x_52);
lean_ctor_set(x_60, 1, x_59);
lean_ctor_set(x_60, 2, x_58);
x_61 = lean_array_push(x_50, x_60);
x_62 = l___aux__Init__Notation______macroRules__stx___x2b__1___closed__8;
x_63 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_63, 0, x_52);
lean_ctor_set(x_63, 1, x_62);
lean_ctor_set(x_63, 2, x_61);
x_64 = lean_array_push(x_50, x_63);
x_65 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__4;
x_66 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_66, 0, x_52);
lean_ctor_set(x_66, 1, x_65);
lean_ctor_set(x_66, 2, x_64);
x_67 = lean_array_push(x_50, x_66);
x_68 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__1;
x_69 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_69, 0, x_52);
lean_ctor_set(x_69, 1, x_68);
lean_ctor_set(x_69, 2, x_67);
x_70 = lean_array_push(x_55, x_47);
x_71 = lean_array_push(x_70, x_69);
x_72 = l_Lean_Parser_Tactic_tacticRepeat_____closed__2;
x_73 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_73, 0, x_52);
lean_ctor_set(x_73, 1, x_72);
lean_ctor_set(x_73, 2, x_71);
x_74 = lean_array_push(x_50, x_73);
x_75 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_75, 0, x_52);
lean_ctor_set(x_75, 1, x_62);
lean_ctor_set(x_75, 2, x_74);
x_76 = lean_array_push(x_50, x_75);
x_77 = l_Lean_Parser_Tactic___aux__Init__Notation______macroRules__Lean__Parser__Tactic__tacticTry____1___closed__2;
x_78 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_78, 0, x_52);
lean_ctor_set(x_78, 1, x_77);
lean_ctor_set(x_78, 2, x_76);
x_79 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_79, 0, x_78);
lean_ctor_set(x_79, 1, x_45);
return x_79;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Tactic_specialize___closed__1() {
_start:
{
@ -47742,6 +48118,26 @@ l_Lean_Parser_Tactic_case___closed__13 = _init_l_Lean_Parser_Tactic_case___close
lean_mark_persistent(l_Lean_Parser_Tactic_case___closed__13);
l_Lean_Parser_Tactic_case = _init_l_Lean_Parser_Tactic_case();
lean_mark_persistent(l_Lean_Parser_Tactic_case);
l_Lean_Parser_Tactic_case_x27___closed__1 = _init_l_Lean_Parser_Tactic_case_x27___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__1);
l_Lean_Parser_Tactic_case_x27___closed__2 = _init_l_Lean_Parser_Tactic_case_x27___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__2);
l_Lean_Parser_Tactic_case_x27___closed__3 = _init_l_Lean_Parser_Tactic_case_x27___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__3);
l_Lean_Parser_Tactic_case_x27___closed__4 = _init_l_Lean_Parser_Tactic_case_x27___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__4);
l_Lean_Parser_Tactic_case_x27___closed__5 = _init_l_Lean_Parser_Tactic_case_x27___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__5);
l_Lean_Parser_Tactic_case_x27___closed__6 = _init_l_Lean_Parser_Tactic_case_x27___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__6);
l_Lean_Parser_Tactic_case_x27___closed__7 = _init_l_Lean_Parser_Tactic_case_x27___closed__7();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__7);
l_Lean_Parser_Tactic_case_x27___closed__8 = _init_l_Lean_Parser_Tactic_case_x27___closed__8();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__8);
l_Lean_Parser_Tactic_case_x27___closed__9 = _init_l_Lean_Parser_Tactic_case_x27___closed__9();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27___closed__9);
l_Lean_Parser_Tactic_case_x27 = _init_l_Lean_Parser_Tactic_case_x27();
lean_mark_persistent(l_Lean_Parser_Tactic_case_x27);
l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__1 = _init_l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__1);
l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__2 = _init_l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__2();
@ -49054,6 +49450,20 @@ l_Lean_Parser_Tactic_dbgTrace___closed__6 = _init_l_Lean_Parser_Tactic_dbgTrace_
lean_mark_persistent(l_Lean_Parser_Tactic_dbgTrace___closed__6);
l_Lean_Parser_Tactic_dbgTrace = _init_l_Lean_Parser_Tactic_dbgTrace();
lean_mark_persistent(l_Lean_Parser_Tactic_dbgTrace);
l_Lean_Parser_Tactic_tacticStop_____closed__1 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__1);
l_Lean_Parser_Tactic_tacticStop_____closed__2 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__2);
l_Lean_Parser_Tactic_tacticStop_____closed__3 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__3);
l_Lean_Parser_Tactic_tacticStop_____closed__4 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__4);
l_Lean_Parser_Tactic_tacticStop_____closed__5 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__5);
l_Lean_Parser_Tactic_tacticStop_____closed__6 = _init_l_Lean_Parser_Tactic_tacticStop_____closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop_____closed__6);
l_Lean_Parser_Tactic_tacticStop__ = _init_l_Lean_Parser_Tactic_tacticStop__();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticStop__);
l_Lean_Parser_Tactic_specialize___closed__1 = _init_l_Lean_Parser_Tactic_specialize___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_specialize___closed__1);
l_Lean_Parser_Tactic_specialize___closed__2 = _init_l_Lean_Parser_Tactic_specialize___closed__2();

190
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -20249,7 +20249,7 @@ return x_2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4(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, uint8_t x_8, uint8_t x_9, uint8_t x_10, 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, lean_object* x_18, lean_object* x_19, lean_object* x_20) {
_start:
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_12);
lean_inc(x_17);
x_21 = l_Lean_Meta_instantiateMVars(x_13, x_16, x_17, x_18, x_19, x_20);
@ -20258,107 +20258,112 @@ lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = l_Lean_Expr_getAppFn(x_22);
x_24 = l_Lean_Expr_consumeMData(x_22);
lean_dec(x_22);
x_25 = l_Lean_Expr_getAppFn(x_24);
lean_dec(x_24);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_14);
lean_inc(x_24);
x_25 = l_Lean_Elab_Term_tryPostponeIfMVar(x_24, x_14, x_15, x_16, x_17, x_18, x_19, x_23);
if (lean_obj_tag(x_25) == 0)
lean_inc(x_25);
x_26 = l_Lean_Elab_Term_tryPostponeIfMVar(x_25, x_14, x_15, x_16, x_17, x_18, x_19, x_23);
if (lean_obj_tag(x_26) == 0)
{
if (lean_obj_tag(x_24) == 4)
{
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; uint8_t x_35;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = lean_ctor_get(x_24, 0);
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_26, 1);
lean_inc(x_27);
lean_dec(x_24);
x_28 = l_Lean_Syntax_getId(x_2);
lean_dec(x_2);
x_29 = lean_erase_macro_scopes(x_28);
x_30 = l_Lean_Name_append(x_27, x_29);
lean_dec(x_27);
x_31 = lean_st_ref_get(x_19, x_26);
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);
x_34 = lean_ctor_get(x_32, 0);
lean_inc(x_34);
lean_dec(x_32);
lean_inc(x_30);
x_35 = l_Lean_Environment_contains(x_34, x_30);
if (x_35 == 0)
lean_dec(x_26);
x_28 = l_Lean_Expr_consumeMData(x_25);
lean_dec(x_25);
if (lean_obj_tag(x_28) == 4)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; uint8_t x_46;
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; lean_object* x_36; uint8_t x_37;
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
lean_dec(x_28);
x_30 = l_Lean_Syntax_getId(x_2);
lean_dec(x_2);
x_31 = lean_erase_macro_scopes(x_30);
x_32 = l_Lean_Name_append(x_29, x_31);
lean_dec(x_29);
x_33 = lean_st_ref_get(x_19, x_27);
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
lean_dec(x_33);
x_36 = lean_ctor_get(x_34, 0);
lean_inc(x_36);
lean_dec(x_34);
lean_inc(x_32);
x_37 = l_Lean_Environment_contains(x_36, x_32);
if (x_37 == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_36 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_36, 0, x_30);
x_37 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__4;
x_38 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
x_39 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__6;
x_38 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_38, 0, x_32);
x_39 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__4;
x_40 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
x_41 = l_Lean_indentExpr(x_1);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__6;
x_42 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
x_43 = l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__8;
x_43 = l_Lean_indentExpr(x_1);
x_44 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
x_45 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_44, x_14, x_15, x_16, x_17, x_18, x_19, x_33);
x_45 = l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__8;
x_46 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
x_47 = l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(x_46, x_14, x_15, x_16, x_17, x_18, x_19, x_35);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
x_46 = !lean_is_exclusive(x_45);
if (x_46 == 0)
x_48 = !lean_is_exclusive(x_47);
if (x_48 == 0)
{
return x_45;
return x_47;
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_47 = lean_ctor_get(x_45, 0);
x_48 = lean_ctor_get(x_45, 1);
lean_inc(x_48);
lean_inc(x_47);
lean_dec(x_45);
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
{
lean_object* x_50; lean_object* x_51;
lean_dec(x_1);
x_50 = lean_box(0);
x_51 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__3(x_30, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_50, x_14, x_15, x_16, x_17, x_18, x_19, x_33);
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_47, 0);
x_50 = lean_ctor_get(x_47, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_47);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
else
{
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_dec(x_24);
lean_object* x_52; lean_object* x_53;
lean_dec(x_1);
x_52 = lean_box(0);
x_53 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__3(x_32, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_52, x_14, x_15, x_16, x_17, x_18, x_19, x_35);
return x_53;
}
}
else
{
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_dec(x_28);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_6);
@ -20366,31 +20371,28 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_52 = lean_ctor_get(x_25, 1);
lean_inc(x_52);
lean_dec(x_25);
x_53 = l_Lean_indentExpr(x_1);
x_54 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__2;
x_55 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
x_56 = l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__8;
x_57 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l_Lean_throwError___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__1(x_57, x_14, x_15, x_16, x_17, x_18, x_19, x_52);
x_54 = l_Lean_indentExpr(x_1);
x_55 = l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___lambda__4___closed__2;
x_56 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_54);
x_57 = l___private_Lean_Elab_App_0__Lean_Elab_Term_mkProjAndCheck___closed__8;
x_58 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
x_59 = l_Lean_throwError___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__1(x_58, x_14, x_15, x_16, x_17, x_18, x_19, x_27);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
return x_58;
return x_59;
}
}
else
{
uint8_t x_59;
lean_dec(x_24);
uint8_t x_60;
lean_dec(x_25);
lean_dec(x_19);
lean_dec(x_18);
lean_dec(x_17);
@ -20405,23 +20407,23 @@ lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_59 = !lean_is_exclusive(x_25);
if (x_59 == 0)
x_60 = !lean_is_exclusive(x_26);
if (x_60 == 0)
{
return x_25;
return x_26;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_25, 0);
x_61 = lean_ctor_get(x_25, 1);
lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_61 = lean_ctor_get(x_26, 0);
x_62 = lean_ctor_get(x_26, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_25);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
lean_dec(x_26);
x_63 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_63, 0, x_61);
lean_ctor_set(x_63, 1, x_62);
return x_63;
}
}
}

280
stage0/stdlib/Lean/Elab/DefView.c generated
View file

@ -14,7 +14,6 @@
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2;
lean_object* l_Lean_Elab_expandOptDeclSig(lean_object*);
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* lean_erase_macro_scopes(lean_object*);
@ -25,7 +24,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__1___closed__1;
LEAN_EXPORT uint8_t l_Lean_Elab_DefKind_isDefOrAbbrevOrOpaque(uint8_t);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4;
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkDefViewOfInstance___spec__5___rarg(lean_object*);
@ -67,6 +65,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkInstanceName___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__2;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__10;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_noConfusion___rarg(uint8_t, uint8_t, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__6;
@ -79,7 +78,6 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___closed__5;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__7;
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_runTermElabM___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1;
lean_object* l_Lean_Elab_mkFreshInstanceName(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_isDefLike___closed__11;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__16;
@ -106,12 +104,10 @@ static lean_object* l_Lean_Elab_Command_mkInstanceName___closed__2;
static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___closed__4;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__11;
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_toCtorIdx(uint8_t);
static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___closed__8;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Char_isLower(uint32_t);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_isDefLike___boxed(lean_object*);
lean_object* l_Nat_repr(lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Elab_instInhabitedDefKind;
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_isTheorem___boxed(lean_object*);
@ -130,6 +126,7 @@ static lean_object* l_Lean_Elab_Command_isDefLike___closed__9;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkDefView___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_toCtorIdx___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instInhabitedDefView;
static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__5___closed__1;
@ -170,10 +167,12 @@ lean_object* l_Lean_Syntax_getKind(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkFreshInstanceName___boxed(lean_object*);
static lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465_(lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3;
static lean_object* l_Lean_Elab_Command_mkInstanceName___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__2;
static lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___closed__2;
static lean_object* l_Lean_Elab_Command_isDefLike___closed__6;
lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
@ -190,11 +189,13 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkDefView___sp
uint8_t l_Lean_Syntax_isNone(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkDefViewOfInstance___spec__10(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Modifiers_addAttribute(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3;
static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__2___closed__1;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__9;
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkInstanceName___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1;
lean_object* l_Lean_Elab_expandOptNamedPrio___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutAutoBoundImplicit___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutErrToSorry___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -213,11 +214,13 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__18;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_DefKind_noConfusion(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__5(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_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1;
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkInstanceName___spec__5___rarg___closed__2;
static lean_object* l_Lean_Elab_Command_mkDefView___closed__1;
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkInstanceName___spec__5___rarg___closed__1;
@ -3757,6 +3760,51 @@ lean_ctor_set(x_15, 1, x_8);
return x_15;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("declValSimple");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
x_2 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(":=");
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___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) {
_start:
{
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; lean_object* x_14; lean_object* x_15;
x_7 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3;
x_8 = l_Lean_mkAtomFrom(x_1, x_7);
x_9 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__12;
x_10 = lean_array_push(x_9, x_8);
x_11 = lean_array_push(x_10, x_3);
x_12 = lean_box(2);
x_13 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2;
x_14 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
lean_ctor_set(x_14, 2, x_11);
x_15 = lean_apply_4(x_2, x_14, x_4, x_5, x_6);
return x_15;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__1() {
_start:
{
@ -3804,33 +3852,29 @@ return x_1;
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("declValSimple");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(2);
x_2 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__10;
x_3 = l_Lean_Elab_instInhabitedDefView___closed__1;
x_4 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
x_2 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__6;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(":=");
x_1 = lean_mk_string("unsafe");
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfConstant(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; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
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; lean_object* x_14;
x_6 = lean_unsigned_to_nat(2u);
x_7 = l_Lean_Syntax_getArg(x_2, x_6);
x_8 = l_Lean_Elab_expandDeclSig(x_7);
@ -3840,65 +3884,117 @@ lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_unsigned_to_nat(3u);
x_12 = l_Lean_Syntax_getArg(x_2, x_11);
x_13 = l_Lean_Syntax_getOptional_x3f(x_12);
lean_dec(x_12);
if (lean_obj_tag(x_13) == 0)
lean_inc(x_9);
lean_inc(x_1);
lean_inc(x_10);
lean_inc(x_2);
x_11 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1___boxed), 8, 4);
lean_closure_set(x_11, 0, x_2);
lean_closure_set(x_11, 1, x_10);
lean_closure_set(x_11, 2, x_1);
lean_closure_set(x_11, 3, x_9);
x_12 = lean_unsigned_to_nat(3u);
x_13 = l_Lean_Syntax_getArg(x_2, x_12);
x_14 = l_Lean_Syntax_getOptional_x3f(x_13);
lean_dec(x_13);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; 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; 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;
x_14 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__11(x_3, x_4, x_5);
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);
x_17 = l_Lean_Elab_Command_getCurrMacroScope(x_3, x_4, x_16);
x_18 = lean_ctor_get(x_17, 1);
uint8_t x_15;
lean_dec(x_10);
lean_dec(x_9);
x_15 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 3);
lean_dec(x_1);
if (x_15 == 0)
{
lean_object* x_16; 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; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_16 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__11(x_3, x_4, x_5);
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_17);
x_19 = l_Lean_Elab_Command_getMainModule___rarg(x_4, x_18);
lean_dec(x_16);
x_19 = l_Lean_Elab_Command_getCurrMacroScope(x_3, x_4, x_18);
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__5;
x_22 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_22, 0, x_15);
lean_ctor_set(x_22, 1, x_21);
x_23 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__11;
x_24 = lean_array_push(x_23, x_22);
x_25 = lean_box(2);
x_26 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__4;
x_27 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
lean_ctor_set(x_27, 2, x_24);
x_28 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__8;
lean_inc(x_2);
x_29 = l_Lean_mkAtomFrom(x_2, x_28);
x_30 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__12;
x_31 = lean_array_push(x_30, x_29);
x_32 = lean_array_push(x_31, x_27);
x_33 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__7;
x_34 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_34, 0, x_25);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set(x_34, 2, x_32);
x_35 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1(x_2, x_10, x_1, x_9, x_34, x_3, x_4, x_20);
lean_dec(x_4);
lean_dec(x_3);
return x_35;
x_21 = l_Lean_Elab_Command_getMainModule___rarg(x_4, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__5;
x_24 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_24, 0, x_17);
lean_ctor_set(x_24, 1, x_23);
x_25 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__12;
x_26 = lean_array_push(x_25, x_24);
x_27 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__6;
x_28 = lean_array_push(x_26, x_27);
x_29 = lean_box(2);
x_30 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__4;
x_31 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
lean_ctor_set(x_31, 2, x_28);
x_32 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2(x_2, x_11, x_31, x_3, x_4, x_22);
return x_32;
}
else
{
lean_object* x_36; lean_object* x_37;
x_36 = lean_ctor_get(x_13, 0);
lean_inc(x_36);
lean_dec(x_13);
x_37 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1(x_2, x_10, x_1, x_9, x_36, x_3, x_4, x_5);
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; 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;
x_33 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__11(x_3, x_4, x_5);
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
lean_dec(x_33);
x_36 = l_Lean_Elab_Command_getCurrMacroScope(x_3, x_4, x_35);
x_37 = lean_ctor_get(x_36, 1);
lean_inc(x_37);
lean_dec(x_36);
x_38 = l_Lean_Elab_Command_getMainModule___rarg(x_4, x_37);
x_39 = lean_ctor_get(x_38, 1);
lean_inc(x_39);
lean_dec(x_38);
x_40 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__5;
lean_inc(x_34);
x_41 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_41, 0, x_34);
lean_ctor_set(x_41, 1, x_40);
x_42 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__7;
x_43 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_43, 0, x_34);
lean_ctor_set(x_43, 1, x_42);
x_44 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__11;
x_45 = lean_array_push(x_44, x_43);
x_46 = lean_box(2);
x_47 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__10;
x_48 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
lean_ctor_set(x_48, 2, x_45);
x_49 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__12;
x_50 = lean_array_push(x_49, x_41);
x_51 = lean_array_push(x_50, x_48);
x_52 = l_Lean_Elab_Command_mkDefViewOfConstant___closed__4;
x_53 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_53, 0, x_46);
lean_ctor_set(x_53, 1, x_52);
lean_ctor_set(x_53, 2, x_51);
x_54 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2(x_2, x_11, x_53, x_3, x_4, x_39);
return x_54;
}
}
else
{
lean_object* x_55; lean_object* x_56;
lean_dec(x_11);
x_55 = lean_ctor_get(x_14, 0);
lean_inc(x_55);
lean_dec(x_14);
x_56 = l_Lean_Elab_Command_mkDefViewOfConstant___lambda__1(x_2, x_10, x_1, x_9, x_55, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_37;
return x_56;
}
}
}
@ -4351,7 +4447,7 @@ lean_dec(x_3);
return x_5;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1() {
_start:
{
lean_object* x_1;
@ -4359,17 +4455,17 @@ x_1 = lean_mk_string("Elab");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____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_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3() {
_start:
{
lean_object* x_1;
@ -4377,21 +4473,21 @@ x_1 = lean_mk_string("definition");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3;
x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__2;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -4536,6 +4632,12 @@ l_Lean_Elab_Command_mkDefViewOfInstance___closed__17 = _init_l_Lean_Elab_Command
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfInstance___closed__17);
l_Lean_Elab_Command_mkDefViewOfInstance___closed__18 = _init_l_Lean_Elab_Command_mkDefViewOfInstance___closed__18();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfInstance___closed__18);
l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__1);
l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__2);
l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___lambda__2___closed__3);
l_Lean_Elab_Command_mkDefViewOfConstant___closed__1 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__1);
l_Lean_Elab_Command_mkDefViewOfConstant___closed__2 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__2();
@ -4550,8 +4652,6 @@ l_Lean_Elab_Command_mkDefViewOfConstant___closed__6 = _init_l_Lean_Elab_Command_
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__6);
l_Lean_Elab_Command_mkDefViewOfConstant___closed__7 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__7();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__7);
l_Lean_Elab_Command_mkDefViewOfConstant___closed__8 = _init_l_Lean_Elab_Command_mkDefViewOfConstant___closed__8();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfConstant___closed__8);
l_Lean_Elab_Command_mkDefViewOfExample___closed__1 = _init_l_Lean_Elab_Command_mkDefViewOfExample___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDefViewOfExample___closed__1);
l_Lean_Elab_Command_mkDefViewOfExample___closed__2 = _init_l_Lean_Elab_Command_mkDefViewOfExample___closed__2();
@ -4582,15 +4682,15 @@ l_Lean_Elab_Command_mkDefView___closed__1 = _init_l_Lean_Elab_Command_mkDefView_
lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__1);
l_Lean_Elab_Command_mkDefView___closed__2 = _init_l_Lean_Elab_Command_mkDefView___closed__2();
lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__2);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__1);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__2);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__3);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383____closed__4);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1383_(lean_io_mk_world());
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__1);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__2();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__2);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__3);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465____closed__4);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1465_(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));

301
stage0/stdlib/Lean/Elab/Extra.c generated
View file

@ -97,6 +97,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOpLazy_declRange_
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_declRange___closed__2;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRelNoProp_declRange___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__12;
@ -161,6 +162,7 @@ static lean_object* l_Lean_Elab_Term_elabForIn_x27___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn_declRange___closed__6;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toTree(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRelNoProp___closed__3;
lean_object* l_Lean_Meta_mkSorry(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabBinRelCore___lambda__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_Lean_Elab_Term_elabForIn___closed__12;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_getMonadForIn___closed__2;
@ -172,15 +174,12 @@ static lean_object* l_Lean_Elab_Term_elabBinRelCore___lambda__3___closed__1;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_Option_get___at_Std_Format_pretty_x27___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_analyze_go___spec__2___closed__4;
static lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2;
lean_object* lean_nat_sub(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__19;
static lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1;
static lean_object* l_Lean_Elab_Term_BinOp_elabBinCalc___closed__1;
static lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_getMonadForIn___closed__5;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(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_Extra_0__Lean_Elab_Term_getMonadForIn___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__3___closed__3;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__17;
lean_object* l_Lean_Expr_headBeta(lean_object*);
@ -253,7 +252,7 @@ static lean_object* l_Lean_Elab_Term_elabBinRelCore_toBoolIfNecessary___closed__
extern lean_object* l_Lean_instInhabitedSyntax;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__3___closed__7;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_toExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5553_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5565_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabBinRel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabForIn_x27___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_Term_elabBinRelCore___lambda__2___closed__5;
@ -369,6 +368,7 @@ lean_object* l_Lean_Meta_mkArrow(lean_object*, lean_object*, lean_object*, lean_
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel_declRange___closed__5;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_elabForIn_x27_declRange___closed__1;
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_BinOp_elabBinOp___closed__4;
lean_object* l_Lean_expandMacros(lean_object*, lean_object*, lean_object*);
@ -388,7 +388,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOpLazy_declRange___closed__6;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___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*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__14;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabBinRelCore_toBoolIfNecessary___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel_declRange___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -402,6 +402,7 @@ static lean_object* l_Lean_Elab_Term_elabForIn___closed__25;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc_declRange(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabBinRelCore_toBoolIfNecessary___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_Term_BinOp_elabDefaultOrNonempty___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_declRange___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc_declRange___closed__7;
@ -454,7 +455,6 @@ static lean_object* l_Lean_Elab_Term_elabForIn___closed__5;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___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*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__2___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Term_BinOp_elabBinOp_declRange___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Extra_0__Lean_Elab_Term_BinOp_hasCoe___boxed(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_Term_BinOp_elabBinOp___closed__5;
static lean_object* l_Lean_Elab_Term_elabForIn___closed__15;
@ -16684,7 +16684,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1() {
_start:
{
lean_object* x_1;
@ -16692,162 +16692,199 @@ x_1 = lean_mk_string("invalid 'default_or_ofNonempty%', expected type is not kno
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2() {
static lean_object* _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1;
x_1 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg(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_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(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_9;
lean_object* x_10;
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);
lean_inc(x_1);
x_9 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_9) == 0)
x_10 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_2, 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)
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2;
x_12 = l_Lean_throwError___at_Lean_Elab_Term_synthesizeInst___spec__1(x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_10);
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2;
x_13 = l_Lean_throwError___at_Lean_Elab_Term_synthesizeInst___spec__1(x_12, 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);
lean_dec(x_4);
return x_12;
return x_13;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_2);
x_13 = lean_ctor_get(x_9, 1);
lean_inc(x_13);
lean_dec(x_9);
x_14 = lean_ctor_get(x_1, 0);
lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_3);
x_14 = lean_ctor_get(x_10, 1);
lean_inc(x_14);
lean_dec(x_1);
lean_dec(x_10);
x_15 = lean_ctor_get(x_2, 0);
lean_inc(x_15);
lean_dec(x_2);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_14);
x_15 = l_Lean_Meta_mkDefault(x_14, x_4, x_5, x_6, x_7, x_13);
if (lean_obj_tag(x_15) == 0)
lean_inc(x_15);
x_16 = l_Lean_Meta_mkDefault(x_15, x_5, x_6, x_7, x_8, x_14);
if (lean_obj_tag(x_16) == 0)
{
lean_dec(x_14);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
return x_15;
}
else
{
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);
x_18 = l_Lean_Meta_mkOfNonempty(x_14, x_4, x_5, x_6, x_7, x_17);
if (lean_obj_tag(x_18) == 0)
{
lean_dec(x_16);
return x_18;
}
else
{
uint8_t x_19;
x_19 = !lean_is_exclusive(x_18);
if (x_19 == 0)
{
lean_object* x_20;
x_20 = lean_ctor_get(x_18, 0);
lean_dec(x_20);
lean_ctor_set(x_18, 0, x_16);
return x_18;
}
else
{
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_18, 1);
lean_inc(x_21);
lean_dec(x_18);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_16);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
}
}
else
{
uint8_t x_23;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_23 = !lean_is_exclusive(x_9);
if (x_23 == 0)
{
return x_9;
return x_16;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_9, 0);
x_25 = lean_ctor_get(x_9, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_9);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(lean_object* x_1) {
_start:
lean_object* x_17; lean_object* x_18; lean_object* x_19;
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);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_15);
x_19 = l_Lean_Meta_mkOfNonempty(x_15, x_5, x_6, x_7, x_8, x_18);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___boxed), 8, 0);
return x_2;
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
return x_19;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___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:
else
{
lean_object* x_9;
x_9 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
uint8_t x_20;
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_21 = lean_ctor_get(x_19, 1);
x_22 = lean_ctor_get(x_19, 0);
lean_dec(x_22);
x_23 = lean_unsigned_to_nat(1u);
x_24 = l_Lean_Syntax_getArg(x_1, x_23);
x_25 = l_Lean_Syntax_isNone(x_24);
lean_dec(x_24);
if (x_25 == 0)
{
uint8_t x_26; lean_object* x_27;
lean_free_object(x_19);
lean_dec(x_17);
x_26 = 0;
x_27 = l_Lean_Meta_mkSorry(x_15, x_26, x_5, x_6, x_7, x_8, x_21);
return x_27;
}
else
{
lean_dec(x_15);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_ctor_set(x_19, 0, x_17);
return x_19;
}
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_28 = lean_ctor_get(x_19, 1);
lean_inc(x_28);
lean_dec(x_19);
x_29 = lean_unsigned_to_nat(1u);
x_30 = l_Lean_Syntax_getArg(x_1, x_29);
x_31 = l_Lean_Syntax_isNone(x_30);
lean_dec(x_30);
if (x_31 == 0)
{
uint8_t x_32; lean_object* x_33;
lean_dec(x_17);
x_32 = 0;
x_33 = l_Lean_Meta_mkSorry(x_15, x_32, x_5, x_6, x_7, x_8, x_28);
return x_33;
}
else
{
lean_object* x_34;
lean_dec(x_15);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_17);
lean_ctor_set(x_34, 1, x_28);
return x_34;
}
}
}
}
}
}
else
{
uint8_t x_35;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
return x_9;
lean_dec(x_2);
x_35 = !lean_is_exclusive(x_10);
if (x_35 == 0)
{
return x_10;
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_10, 0);
x_37 = lean_ctor_get(x_10, 1);
lean_inc(x_37);
lean_inc(x_36);
lean_dec(x_10);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
return x_38;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___boxed(lean_object* x_1) {
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___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_2;
x_2 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(x_1);
lean_object* x_10;
x_10 = l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty(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_1);
return x_2;
return x_10;
}
}
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1() {
@ -16890,7 +16927,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonem
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___boxed), 9, 0);
return x_1;
}
}
@ -16922,8 +16959,8 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonem
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(353u);
x_2 = lean_unsigned_to_nat(14u);
x_1 = lean_unsigned_to_nat(358u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -16937,7 +16974,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty_declRange___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty_declRange___closed__2;
x_4 = lean_unsigned_to_nat(14u);
x_4 = lean_unsigned_to_nat(34u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -17008,7 +17045,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5553_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5565_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -17548,10 +17585,10 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc_declRange__
res = l___regBuiltin_Lean_Elab_Term_BinOp_elabBinCalc_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__1);
l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___rarg___closed__2);
l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1 = _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1);
l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2 = _init_l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2);
l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__1);
l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty___closed__2();
@ -17582,7 +17619,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty_d
res = l___regBuiltin_Lean_Elab_Term_BinOp_elabDefaultOrNonempty_declRange(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5553_(lean_io_mk_world());
res = l_Lean_Elab_Term_BinOp_initFn____x40_Lean_Elab_Extra___hyg_5565_(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));

6764
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

File diff suppressed because it is too large Load diff

241
stage0/stdlib/Lean/Elab/PreDefinition/WF/Rel.c generated
View file

@ -6502,11 +6502,11 @@ x_52 = lean_ctor_get(x_38, 0);
lean_dec(x_52);
x_53 = lean_nat_add(x_44, x_46);
lean_ctor_set(x_38, 0, x_53);
x_54 = lean_ctor_get(x_39, 0);
x_54 = lean_ctor_get(x_42, 0);
lean_inc(x_54);
x_55 = lean_ctor_get(x_39, 1);
x_55 = lean_ctor_get(x_42, 1);
lean_inc(x_55);
x_56 = lean_ctor_get(x_39, 2);
x_56 = lean_ctor_get(x_42, 2);
lean_inc(x_56);
x_57 = lean_nat_dec_lt(x_55, x_56);
if (x_57 == 0)
@ -6526,26 +6526,26 @@ goto block_33;
else
{
uint8_t x_59;
x_59 = !lean_is_exclusive(x_39);
x_59 = !lean_is_exclusive(x_42);
if (x_59 == 0)
{
lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; uint8_t x_69;
x_60 = lean_ctor_get(x_39, 2);
x_60 = lean_ctor_get(x_42, 2);
lean_dec(x_60);
x_61 = lean_ctor_get(x_39, 1);
x_61 = lean_ctor_get(x_42, 1);
lean_dec(x_61);
x_62 = lean_ctor_get(x_39, 0);
x_62 = lean_ctor_get(x_42, 0);
lean_dec(x_62);
x_63 = lean_array_fget(x_54, x_55);
x_64 = lean_unsigned_to_nat(1u);
x_65 = lean_nat_add(x_55, x_64);
lean_dec(x_55);
lean_ctor_set(x_39, 1, x_65);
x_66 = lean_ctor_get(x_42, 0);
lean_ctor_set(x_42, 1, x_65);
x_66 = lean_ctor_get(x_39, 0);
lean_inc(x_66);
x_67 = lean_ctor_get(x_42, 1);
x_67 = lean_ctor_get(x_39, 1);
lean_inc(x_67);
x_68 = lean_ctor_get(x_42, 2);
x_68 = lean_ctor_get(x_39, 2);
lean_inc(x_68);
x_69 = lean_nat_dec_lt(x_67, x_68);
if (x_69 == 0)
@ -6569,20 +6569,20 @@ uint8_t x_71;
lean_free_object(x_37);
lean_free_object(x_14);
lean_free_object(x_34);
x_71 = !lean_is_exclusive(x_42);
x_71 = !lean_is_exclusive(x_39);
if (x_71 == 0)
{
lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; uint8_t x_84;
x_72 = lean_ctor_get(x_42, 2);
x_72 = lean_ctor_get(x_39, 2);
lean_dec(x_72);
x_73 = lean_ctor_get(x_42, 1);
x_73 = lean_ctor_get(x_39, 1);
lean_dec(x_73);
x_74 = lean_ctor_get(x_42, 0);
x_74 = lean_ctor_get(x_39, 0);
lean_dec(x_74);
x_75 = lean_array_fget(x_66, x_67);
x_76 = lean_nat_add(x_67, x_64);
lean_dec(x_67);
lean_ctor_set(x_42, 1, x_76);
lean_ctor_set(x_39, 1, x_76);
lean_inc(x_6);
lean_inc(x_8);
x_77 = lean_array_push(x_8, x_6);
@ -6827,7 +6827,7 @@ goto block_33;
else
{
lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; uint8_t x_187;
lean_dec(x_42);
lean_dec(x_39);
x_177 = lean_array_fget(x_66, x_67);
x_178 = lean_nat_add(x_67, x_64);
lean_dec(x_67);
@ -6926,7 +6926,7 @@ x_216 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_216, 0, x_210);
lean_ctor_set(x_216, 1, x_198);
lean_ctor_set(x_216, 2, x_215);
x_217 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_185, x_179, x_38, x_39, x_43, x_216, x_15, x_16, x_17, x_18, x_19, x_20, x_194);
x_217 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_185, x_42, x_38, x_179, x_43, x_216, x_15, x_16, x_17, x_18, x_19, x_20, x_194);
lean_dec(x_24);
x_218 = lean_ctor_get(x_217, 0);
lean_inc(x_218);
@ -7064,7 +7064,7 @@ x_276 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_276, 0, x_246);
lean_ctor_set(x_276, 1, x_230);
lean_ctor_set(x_276, 2, x_275);
x_277 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_185, x_179, x_38, x_39, x_43, x_276, x_15, x_16, x_17, x_18, x_19, x_20, x_226);
x_277 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_185, x_42, x_38, x_179, x_43, x_276, x_15, x_16, x_17, x_18, x_19, x_20, x_226);
lean_dec(x_24);
x_278 = lean_ctor_get(x_277, 0);
lean_inc(x_278);
@ -7081,7 +7081,7 @@ goto block_33;
else
{
lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; uint8_t x_287;
lean_dec(x_39);
lean_dec(x_42);
x_280 = lean_array_fget(x_54, x_55);
x_281 = lean_unsigned_to_nat(1u);
x_282 = lean_nat_add(x_55, x_281);
@ -7090,11 +7090,11 @@ x_283 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_283, 0, x_54);
lean_ctor_set(x_283, 1, x_282);
lean_ctor_set(x_283, 2, x_56);
x_284 = lean_ctor_get(x_42, 0);
x_284 = lean_ctor_get(x_39, 0);
lean_inc(x_284);
x_285 = lean_ctor_get(x_42, 1);
x_285 = lean_ctor_get(x_39, 1);
lean_inc(x_285);
x_286 = lean_ctor_get(x_42, 2);
x_286 = lean_ctor_get(x_39, 2);
lean_inc(x_286);
x_287 = lean_nat_dec_lt(x_285, x_286);
if (x_287 == 0)
@ -7106,7 +7106,7 @@ lean_dec(x_284);
lean_dec(x_280);
lean_dec(x_44);
lean_dec(x_24);
lean_ctor_set(x_14, 0, x_283);
lean_ctor_set(x_37, 0, x_283);
x_288 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_288, 0, x_14);
x_25 = x_288;
@ -7119,13 +7119,13 @@ lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292;
lean_free_object(x_37);
lean_free_object(x_14);
lean_free_object(x_34);
if (lean_is_exclusive(x_42)) {
lean_ctor_release(x_42, 0);
lean_ctor_release(x_42, 1);
lean_ctor_release(x_42, 2);
x_289 = x_42;
if (lean_is_exclusive(x_39)) {
lean_ctor_release(x_39, 0);
lean_ctor_release(x_39, 1);
lean_ctor_release(x_39, 2);
x_289 = x_39;
} else {
lean_dec_ref(x_42);
lean_dec_ref(x_39);
x_289 = lean_box(0);
}
x_290 = lean_array_fget(x_284, x_285);
@ -7230,7 +7230,7 @@ x_329 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_329, 0, x_323);
lean_ctor_set(x_329, 1, x_311);
lean_ctor_set(x_329, 2, x_328);
x_330 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_298, x_292, x_38, x_283, x_43, x_329, x_15, x_16, x_17, x_18, x_19, x_20, x_307);
x_330 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_298, x_283, x_38, x_292, x_43, x_329, x_15, x_16, x_17, x_18, x_19, x_20, x_307);
lean_dec(x_24);
x_331 = lean_ctor_get(x_330, 0);
lean_inc(x_331);
@ -7368,7 +7368,7 @@ x_389 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_389, 0, x_359);
lean_ctor_set(x_389, 1, x_343);
lean_ctor_set(x_389, 2, x_388);
x_390 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_298, x_292, x_38, x_283, x_43, x_389, x_15, x_16, x_17, x_18, x_19, x_20, x_339);
x_390 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_298, x_283, x_38, x_292, x_43, x_389, x_15, x_16, x_17, x_18, x_19, x_20, x_339);
lean_dec(x_24);
x_391 = lean_ctor_get(x_390, 0);
lean_inc(x_391);
@ -7392,11 +7392,11 @@ x_394 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_394, 0, x_393);
lean_ctor_set(x_394, 1, x_45);
lean_ctor_set(x_394, 2, x_46);
x_395 = lean_ctor_get(x_39, 0);
x_395 = lean_ctor_get(x_42, 0);
lean_inc(x_395);
x_396 = lean_ctor_get(x_39, 1);
x_396 = lean_ctor_get(x_42, 1);
lean_inc(x_396);
x_397 = lean_ctor_get(x_39, 2);
x_397 = lean_ctor_get(x_42, 2);
lean_inc(x_397);
x_398 = lean_nat_dec_lt(x_396, x_397);
if (x_398 == 0)
@ -7417,13 +7417,13 @@ goto block_33;
else
{
lean_object* x_400; lean_object* x_401; lean_object* x_402; lean_object* x_403; lean_object* x_404; lean_object* x_405; lean_object* x_406; lean_object* x_407; uint8_t x_408;
if (lean_is_exclusive(x_39)) {
lean_ctor_release(x_39, 0);
lean_ctor_release(x_39, 1);
lean_ctor_release(x_39, 2);
x_400 = x_39;
if (lean_is_exclusive(x_42)) {
lean_ctor_release(x_42, 0);
lean_ctor_release(x_42, 1);
lean_ctor_release(x_42, 2);
x_400 = x_42;
} else {
lean_dec_ref(x_39);
lean_dec_ref(x_42);
x_400 = lean_box(0);
}
x_401 = lean_array_fget(x_395, x_396);
@ -7438,11 +7438,11 @@ if (lean_is_scalar(x_400)) {
lean_ctor_set(x_404, 0, x_395);
lean_ctor_set(x_404, 1, x_403);
lean_ctor_set(x_404, 2, x_397);
x_405 = lean_ctor_get(x_42, 0);
x_405 = lean_ctor_get(x_39, 0);
lean_inc(x_405);
x_406 = lean_ctor_get(x_42, 1);
x_406 = lean_ctor_get(x_39, 1);
lean_inc(x_406);
x_407 = lean_ctor_get(x_42, 2);
x_407 = lean_ctor_get(x_39, 2);
lean_inc(x_407);
x_408 = lean_nat_dec_lt(x_406, x_407);
if (x_408 == 0)
@ -7454,8 +7454,8 @@ lean_dec(x_405);
lean_dec(x_401);
lean_dec(x_44);
lean_dec(x_24);
lean_ctor_set(x_37, 0, x_404);
lean_ctor_set(x_34, 0, x_394);
lean_ctor_set(x_14, 0, x_404);
x_409 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_409, 0, x_14);
x_25 = x_409;
@ -7468,13 +7468,13 @@ lean_object* x_410; lean_object* x_411; lean_object* x_412; lean_object* x_413;
lean_free_object(x_37);
lean_free_object(x_14);
lean_free_object(x_34);
if (lean_is_exclusive(x_42)) {
lean_ctor_release(x_42, 0);
lean_ctor_release(x_42, 1);
lean_ctor_release(x_42, 2);
x_410 = x_42;
if (lean_is_exclusive(x_39)) {
lean_ctor_release(x_39, 0);
lean_ctor_release(x_39, 1);
lean_ctor_release(x_39, 2);
x_410 = x_39;
} else {
lean_dec_ref(x_42);
lean_dec_ref(x_39);
x_410 = lean_box(0);
}
x_411 = lean_array_fget(x_405, x_406);
@ -7579,7 +7579,7 @@ x_450 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_450, 0, x_444);
lean_ctor_set(x_450, 1, x_432);
lean_ctor_set(x_450, 2, x_449);
x_451 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_419, x_413, x_394, x_404, x_43, x_450, x_15, x_16, x_17, x_18, x_19, x_20, x_428);
x_451 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_419, x_404, x_394, x_413, x_43, x_450, x_15, x_16, x_17, x_18, x_19, x_20, x_428);
lean_dec(x_24);
x_452 = lean_ctor_get(x_451, 0);
lean_inc(x_452);
@ -7717,7 +7717,7 @@ x_510 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_510, 0, x_480);
lean_ctor_set(x_510, 1, x_464);
lean_ctor_set(x_510, 2, x_509);
x_511 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_419, x_413, x_394, x_404, x_43, x_510, x_15, x_16, x_17, x_18, x_19, x_20, x_460);
x_511 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_419, x_404, x_394, x_413, x_43, x_510, x_15, x_16, x_17, x_18, x_19, x_20, x_460);
lean_dec(x_24);
x_512 = lean_ctor_get(x_511, 0);
lean_inc(x_512);
@ -7786,11 +7786,11 @@ if (lean_is_scalar(x_522)) {
lean_ctor_set(x_524, 0, x_523);
lean_ctor_set(x_524, 1, x_517);
lean_ctor_set(x_524, 2, x_518);
x_525 = lean_ctor_get(x_39, 0);
x_525 = lean_ctor_get(x_514, 0);
lean_inc(x_525);
x_526 = lean_ctor_get(x_39, 1);
x_526 = lean_ctor_get(x_514, 1);
lean_inc(x_526);
x_527 = lean_ctor_get(x_39, 2);
x_527 = lean_ctor_get(x_514, 2);
lean_inc(x_527);
x_528 = lean_nat_dec_lt(x_526, x_527);
if (x_528 == 0)
@ -7815,13 +7815,13 @@ goto block_33;
else
{
lean_object* x_531; lean_object* x_532; lean_object* x_533; lean_object* x_534; lean_object* x_535; lean_object* x_536; lean_object* x_537; lean_object* x_538; uint8_t x_539;
if (lean_is_exclusive(x_39)) {
lean_ctor_release(x_39, 0);
lean_ctor_release(x_39, 1);
lean_ctor_release(x_39, 2);
x_531 = x_39;
if (lean_is_exclusive(x_514)) {
lean_ctor_release(x_514, 0);
lean_ctor_release(x_514, 1);
lean_ctor_release(x_514, 2);
x_531 = x_514;
} else {
lean_dec_ref(x_39);
lean_dec_ref(x_514);
x_531 = lean_box(0);
}
x_532 = lean_array_fget(x_525, x_526);
@ -7836,11 +7836,11 @@ if (lean_is_scalar(x_531)) {
lean_ctor_set(x_535, 0, x_525);
lean_ctor_set(x_535, 1, x_534);
lean_ctor_set(x_535, 2, x_527);
x_536 = lean_ctor_get(x_514, 0);
x_536 = lean_ctor_get(x_39, 0);
lean_inc(x_536);
x_537 = lean_ctor_get(x_514, 1);
x_537 = lean_ctor_get(x_39, 1);
lean_inc(x_537);
x_538 = lean_ctor_get(x_514, 2);
x_538 = lean_ctor_get(x_39, 2);
lean_inc(x_538);
x_539 = lean_nat_dec_lt(x_537, x_538);
if (x_539 == 0)
@ -7853,11 +7853,10 @@ lean_dec(x_532);
lean_dec(x_516);
lean_dec(x_24);
x_540 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_540, 0, x_514);
lean_ctor_set(x_540, 0, x_535);
lean_ctor_set(x_540, 1, x_515);
lean_ctor_set(x_34, 1, x_540);
lean_ctor_set(x_34, 0, x_524);
lean_ctor_set(x_14, 0, x_535);
x_541 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_541, 0, x_14);
x_25 = x_541;
@ -7869,13 +7868,13 @@ else
lean_object* x_542; lean_object* x_543; lean_object* x_544; lean_object* x_545; lean_object* x_546; lean_object* x_547; lean_object* x_548; lean_object* x_549; lean_object* x_550; lean_object* x_551; lean_object* x_552; uint8_t x_553;
lean_free_object(x_14);
lean_free_object(x_34);
if (lean_is_exclusive(x_514)) {
lean_ctor_release(x_514, 0);
lean_ctor_release(x_514, 1);
lean_ctor_release(x_514, 2);
x_542 = x_514;
if (lean_is_exclusive(x_39)) {
lean_ctor_release(x_39, 0);
lean_ctor_release(x_39, 1);
lean_ctor_release(x_39, 2);
x_542 = x_39;
} else {
lean_dec_ref(x_514);
lean_dec_ref(x_39);
x_542 = lean_box(0);
}
x_543 = lean_array_fget(x_536, x_537);
@ -7980,7 +7979,7 @@ x_582 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_582, 0, x_576);
lean_ctor_set(x_582, 1, x_564);
lean_ctor_set(x_582, 2, x_581);
x_583 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_551, x_545, x_524, x_535, x_515, x_582, x_15, x_16, x_17, x_18, x_19, x_20, x_560);
x_583 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_551, x_535, x_524, x_545, x_515, x_582, x_15, x_16, x_17, x_18, x_19, x_20, x_560);
lean_dec(x_24);
x_584 = lean_ctor_get(x_583, 0);
lean_inc(x_584);
@ -8118,7 +8117,7 @@ x_642 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_642, 0, x_612);
lean_ctor_set(x_642, 1, x_596);
lean_ctor_set(x_642, 2, x_641);
x_643 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_551, x_545, x_524, x_535, x_515, x_642, x_15, x_16, x_17, x_18, x_19, x_20, x_592);
x_643 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_551, x_535, x_524, x_545, x_515, x_642, x_15, x_16, x_17, x_18, x_19, x_20, x_592);
lean_dec(x_24);
x_644 = lean_ctor_get(x_643, 0);
lean_inc(x_644);
@ -8206,11 +8205,11 @@ if (lean_is_scalar(x_659)) {
lean_ctor_set(x_661, 0, x_660);
lean_ctor_set(x_661, 1, x_653);
lean_ctor_set(x_661, 2, x_654);
x_662 = lean_ctor_get(x_648, 0);
x_662 = lean_ctor_get(x_649, 0);
lean_inc(x_662);
x_663 = lean_ctor_get(x_648, 1);
x_663 = lean_ctor_get(x_649, 1);
lean_inc(x_663);
x_664 = lean_ctor_get(x_648, 2);
x_664 = lean_ctor_get(x_649, 2);
lean_inc(x_664);
x_665 = lean_nat_dec_lt(x_663, x_664);
if (x_665 == 0)
@ -8242,13 +8241,13 @@ goto block_33;
else
{
lean_object* x_669; lean_object* x_670; lean_object* x_671; lean_object* x_672; lean_object* x_673; lean_object* x_674; lean_object* x_675; lean_object* x_676; uint8_t x_677;
if (lean_is_exclusive(x_648)) {
lean_ctor_release(x_648, 0);
lean_ctor_release(x_648, 1);
lean_ctor_release(x_648, 2);
x_669 = x_648;
if (lean_is_exclusive(x_649)) {
lean_ctor_release(x_649, 0);
lean_ctor_release(x_649, 1);
lean_ctor_release(x_649, 2);
x_669 = x_649;
} else {
lean_dec_ref(x_648);
lean_dec_ref(x_649);
x_669 = lean_box(0);
}
x_670 = lean_array_fget(x_662, x_663);
@ -8263,11 +8262,11 @@ if (lean_is_scalar(x_669)) {
lean_ctor_set(x_673, 0, x_662);
lean_ctor_set(x_673, 1, x_672);
lean_ctor_set(x_673, 2, x_664);
x_674 = lean_ctor_get(x_649, 0);
x_674 = lean_ctor_get(x_648, 0);
lean_inc(x_674);
x_675 = lean_ctor_get(x_649, 1);
x_675 = lean_ctor_get(x_648, 1);
lean_inc(x_675);
x_676 = lean_ctor_get(x_649, 2);
x_676 = lean_ctor_get(x_648, 2);
lean_inc(x_676);
x_677 = lean_nat_dec_lt(x_675, x_676);
if (x_677 == 0)
@ -8284,12 +8283,12 @@ if (lean_is_scalar(x_651)) {
} else {
x_678 = x_651;
}
lean_ctor_set(x_678, 0, x_649);
lean_ctor_set(x_678, 0, x_673);
lean_ctor_set(x_678, 1, x_650);
lean_ctor_set(x_34, 1, x_678);
lean_ctor_set(x_34, 0, x_661);
x_679 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_679, 0, x_673);
lean_ctor_set(x_679, 0, x_648);
lean_ctor_set(x_679, 1, x_34);
x_680 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_680, 0, x_679);
@ -8302,13 +8301,13 @@ else
lean_object* x_681; lean_object* x_682; lean_object* x_683; lean_object* x_684; lean_object* x_685; lean_object* x_686; lean_object* x_687; lean_object* x_688; lean_object* x_689; lean_object* x_690; lean_object* x_691; uint8_t x_692;
lean_dec(x_651);
lean_free_object(x_34);
if (lean_is_exclusive(x_649)) {
lean_ctor_release(x_649, 0);
lean_ctor_release(x_649, 1);
lean_ctor_release(x_649, 2);
x_681 = x_649;
if (lean_is_exclusive(x_648)) {
lean_ctor_release(x_648, 0);
lean_ctor_release(x_648, 1);
lean_ctor_release(x_648, 2);
x_681 = x_648;
} else {
lean_dec_ref(x_649);
lean_dec_ref(x_648);
x_681 = lean_box(0);
}
x_682 = lean_array_fget(x_674, x_675);
@ -8413,7 +8412,7 @@ x_721 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_721, 0, x_715);
lean_ctor_set(x_721, 1, x_703);
lean_ctor_set(x_721, 2, x_720);
x_722 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_690, x_684, x_661, x_673, x_650, x_721, x_15, x_16, x_17, x_18, x_19, x_20, x_699);
x_722 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_690, x_673, x_661, x_684, x_650, x_721, x_15, x_16, x_17, x_18, x_19, x_20, x_699);
lean_dec(x_24);
x_723 = lean_ctor_get(x_722, 0);
lean_inc(x_723);
@ -8551,7 +8550,7 @@ x_781 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_781, 0, x_751);
lean_ctor_set(x_781, 1, x_735);
lean_ctor_set(x_781, 2, x_780);
x_782 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_690, x_684, x_661, x_673, x_650, x_781, x_15, x_16, x_17, x_18, x_19, x_20, x_731);
x_782 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_690, x_673, x_661, x_684, x_650, x_781, x_15, x_16, x_17, x_18, x_19, x_20, x_731);
lean_dec(x_24);
x_783 = lean_ctor_get(x_782, 0);
lean_inc(x_783);
@ -8655,11 +8654,11 @@ if (lean_is_scalar(x_800)) {
lean_ctor_set(x_802, 0, x_801);
lean_ctor_set(x_802, 1, x_793);
lean_ctor_set(x_802, 2, x_794);
x_803 = lean_ctor_get(x_787, 0);
x_803 = lean_ctor_get(x_789, 0);
lean_inc(x_803);
x_804 = lean_ctor_get(x_787, 1);
x_804 = lean_ctor_get(x_789, 1);
lean_inc(x_804);
x_805 = lean_ctor_get(x_787, 2);
x_805 = lean_ctor_get(x_789, 2);
lean_inc(x_805);
x_806 = lean_nat_dec_lt(x_804, x_805);
if (x_806 == 0)
@ -8696,13 +8695,13 @@ goto block_33;
else
{
lean_object* x_811; lean_object* x_812; lean_object* x_813; lean_object* x_814; lean_object* x_815; lean_object* x_816; lean_object* x_817; lean_object* x_818; uint8_t x_819;
if (lean_is_exclusive(x_787)) {
lean_ctor_release(x_787, 0);
lean_ctor_release(x_787, 1);
lean_ctor_release(x_787, 2);
x_811 = x_787;
if (lean_is_exclusive(x_789)) {
lean_ctor_release(x_789, 0);
lean_ctor_release(x_789, 1);
lean_ctor_release(x_789, 2);
x_811 = x_789;
} else {
lean_dec_ref(x_787);
lean_dec_ref(x_789);
x_811 = lean_box(0);
}
x_812 = lean_array_fget(x_803, x_804);
@ -8717,11 +8716,11 @@ if (lean_is_scalar(x_811)) {
lean_ctor_set(x_815, 0, x_803);
lean_ctor_set(x_815, 1, x_814);
lean_ctor_set(x_815, 2, x_805);
x_816 = lean_ctor_get(x_789, 0);
x_816 = lean_ctor_get(x_787, 0);
lean_inc(x_816);
x_817 = lean_ctor_get(x_789, 1);
x_817 = lean_ctor_get(x_787, 1);
lean_inc(x_817);
x_818 = lean_ctor_get(x_789, 2);
x_818 = lean_ctor_get(x_787, 2);
lean_inc(x_818);
x_819 = lean_nat_dec_lt(x_817, x_818);
if (x_819 == 0)
@ -8738,7 +8737,7 @@ if (lean_is_scalar(x_791)) {
} else {
x_820 = x_791;
}
lean_ctor_set(x_820, 0, x_789);
lean_ctor_set(x_820, 0, x_815);
lean_ctor_set(x_820, 1, x_790);
x_821 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_821, 0, x_802);
@ -8748,7 +8747,7 @@ if (lean_is_scalar(x_788)) {
} else {
x_822 = x_788;
}
lean_ctor_set(x_822, 0, x_815);
lean_ctor_set(x_822, 0, x_787);
lean_ctor_set(x_822, 1, x_821);
x_823 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_823, 0, x_822);
@ -8761,13 +8760,13 @@ else
lean_object* x_824; lean_object* x_825; lean_object* x_826; lean_object* x_827; lean_object* x_828; lean_object* x_829; lean_object* x_830; lean_object* x_831; lean_object* x_832; lean_object* x_833; lean_object* x_834; uint8_t x_835;
lean_dec(x_791);
lean_dec(x_788);
if (lean_is_exclusive(x_789)) {
lean_ctor_release(x_789, 0);
lean_ctor_release(x_789, 1);
lean_ctor_release(x_789, 2);
x_824 = x_789;
if (lean_is_exclusive(x_787)) {
lean_ctor_release(x_787, 0);
lean_ctor_release(x_787, 1);
lean_ctor_release(x_787, 2);
x_824 = x_787;
} else {
lean_dec_ref(x_789);
lean_dec_ref(x_787);
x_824 = lean_box(0);
}
x_825 = lean_array_fget(x_816, x_817);
@ -8872,7 +8871,7 @@ x_864 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_864, 0, x_858);
lean_ctor_set(x_864, 1, x_846);
lean_ctor_set(x_864, 2, x_863);
x_865 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_833, x_827, x_802, x_815, x_790, x_864, x_15, x_16, x_17, x_18, x_19, x_20, x_842);
x_865 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_833, x_815, x_802, x_827, x_790, x_864, x_15, x_16, x_17, x_18, x_19, x_20, x_842);
lean_dec(x_24);
x_866 = lean_ctor_get(x_865, 0);
lean_inc(x_866);
@ -9010,7 +9009,7 @@ x_924 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_924, 0, x_894);
lean_ctor_set(x_924, 1, x_878);
lean_ctor_set(x_924, 2, x_923);
x_925 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_833, x_827, x_802, x_815, x_790, x_924, x_15, x_16, x_17, x_18, x_19, x_20, x_874);
x_925 = l_Array_forInUnsafe_loop___at_Lean_Elab_WF_elabWFRel_generateElements___spec__2___lambda__1(x_24, x_833, x_815, x_802, x_827, x_790, x_924, x_15, x_16, x_17, x_18, x_19, x_20, x_874);
lean_dec(x_24);
x_926 = lean_ctor_get(x_925, 0);
lean_inc(x_926);
@ -9254,13 +9253,13 @@ lean_ctor_set(x_44, 1, x_42);
lean_ctor_set(x_44, 2, x_43);
x_45 = l___private_Lean_Elab_PreDefinition_WF_Rel_0__Lean_Elab_WF_unpackMutual_go___closed__1;
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_39);
lean_ctor_set(x_46, 0, x_41);
lean_ctor_set(x_46, 1, x_45);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_44);
lean_ctor_set(x_47, 1, x_46);
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_41);
lean_ctor_set(x_48, 0, x_39);
lean_ctor_set(x_48, 1, x_47);
x_49 = lean_usize_of_nat(x_42);
x_50 = 0;

477
stage0/stdlib/Lean/Elab/Structure.c generated
View file

@ -65,6 +65,7 @@ static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStr
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getNestedProjectionArg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_userName(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__12(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_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go(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_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__6___closed__7;
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_NameSet_contains___boxed(lean_object*, lean_object*);
@ -128,7 +129,6 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldInfo____x40_Lean_Elab_Structure___hyg_551____closed__15;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkToParentName_go(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyDefaultValue_x3f_failed___closed__2;
static size_t l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___closed__4;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -136,6 +136,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___priva
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldInfo____x40_Lean_Elab_Structure___hyg_551____closed__18;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults(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_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__3;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___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*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_go___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__15___closed__2;
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldInfo____x40_Lean_Elab_Structure___hyg_551____closed__3;
@ -504,7 +505,6 @@ static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___closed__1;
static lean_object* l_Lean_Elab_Command_elabStructure___closed__5;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_processOveriddenDefaultValues___spec__1(lean_object*, 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_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(lean_object*, 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_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___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_EXPORT lean_object* l_Lean_Elab_getOptDerivingClasses___at_Lean_Elab_Command_elabStructure___spec__2___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -726,6 +726,7 @@ static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStr
lean_object* l_Lean_getStructureCtor(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_go___rarg___lambda__4___closed__3;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_registerStructure___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_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___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___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldKind____x40_Lean_Elab_Structure___hyg_342____closed__16;
lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
static lean_object* l_Lean_Elab_Command_checkValidFieldModifier___closed__2;
@ -778,7 +779,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_getOptDerivingClasses___at_Lean_Elab_Comman
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_go___rarg___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*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__6___closed__6;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_copyFields_copy___rarg___lambda__5___boxed(lean_object**);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10848_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10951_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_2573_(lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldInfo____x40_Lean_Elab_Structure___hyg_551____closed__20;
@ -939,6 +940,7 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Term_synthesizeInst___spec__1(lean
lean_object* l_panic___at_Lean_ResolveName_resolveNamespaceUsingScope___spec__1(lean_object*);
lean_object* l_Lean_setEnv___at_Lean_Elab_Term_evalExpr___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___spec__1(lean_object*, 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_EXPORT lean_object* l_Lean_Elab_Command_elabStructure___lambda__3___boxed(lean_object**);
LEAN_EXPORT lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__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_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__2___closed__4;
@ -18522,252 +18524,332 @@ return x_30;
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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* 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) {
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___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* 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, lean_object* x_14) {
_start:
{
uint8_t x_14;
x_14 = lean_usize_dec_eq(x_4, x_5);
if (x_14 == 0)
uint8_t x_15;
x_15 = lean_usize_dec_lt(x_5, x_4);
if (x_15 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_array_uget(x_3, x_4);
x_16 = lean_ctor_get(x_15, 2);
lean_inc(x_16);
lean_dec(x_15);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
x_17 = lean_infer_type(x_16, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_17) == 0)
lean_object* x_16;
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_2);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_6);
lean_ctor_set(x_16, 1, x_14);
return x_16;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_17, 0);
lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_dec(x_6);
x_17 = lean_array_uget(x_3, x_5);
x_18 = lean_ctor_get(x_17, 2);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
x_20 = l_Lean_Meta_getLevel(x_18, x_9, x_10, x_11, x_12, x_19);
if (lean_obj_tag(x_20) == 0)
x_19 = lean_infer_type(x_18, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_19) == 0)
{
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_21 = lean_ctor_get(x_20, 0);
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
x_23 = l_Lean_MetavarContext_instantiateLevelMVars___at_Lean_Meta_instantiateLevelMVars___spec__1(x_21, x_9, x_10, x_11, x_12, x_22);
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec(x_23);
lean_dec(x_19);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_7);
lean_inc(x_2);
lean_inc(x_1);
x_26 = l_Lean_Elab_Command_accLevelAtCtor(x_24, x_1, x_2, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_25);
if (lean_obj_tag(x_26) == 0)
x_22 = l_Lean_Meta_getLevel(x_20, x_10, x_11, x_12, x_13, x_21);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_27; lean_object* x_28; size_t x_29; size_t x_30;
x_27 = lean_ctor_get(x_26, 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;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = l_Lean_MetavarContext_instantiateLevelMVars___at_Lean_Meta_instantiateLevelMVars___spec__1(x_23, x_10, x_11, x_12, x_13, x_24);
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
x_29 = 1;
x_30 = lean_usize_add(x_4, x_29);
x_4 = x_30;
x_6 = x_27;
x_13 = x_28;
lean_dec(x_25);
lean_inc(x_12);
lean_inc(x_10);
lean_inc(x_8);
lean_inc(x_2);
x_28 = l_Lean_Elab_Command_accLevelAtCtor(x_26, x_1, x_2, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_27);
if (lean_obj_tag(x_28) == 0)
{
lean_object* x_29; size_t x_30; size_t x_31; lean_object* x_32;
x_29 = lean_ctor_get(x_28, 1);
lean_inc(x_29);
lean_dec(x_28);
x_30 = 1;
x_31 = lean_usize_add(x_5, x_30);
x_32 = lean_box(0);
x_5 = x_31;
x_6 = x_32;
x_14 = x_29;
goto _start;
}
else
{
uint8_t x_32;
uint8_t x_34;
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_32 = !lean_is_exclusive(x_26);
if (x_32 == 0)
x_34 = !lean_is_exclusive(x_28);
if (x_34 == 0)
{
return x_26;
return x_28;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_26, 0);
x_34 = lean_ctor_get(x_26, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_26);
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;
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_28, 0);
x_36 = lean_ctor_get(x_28, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_28);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
}
}
}
else
{
uint8_t x_36;
uint8_t x_38;
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_36 = !lean_is_exclusive(x_20);
if (x_36 == 0)
x_38 = !lean_is_exclusive(x_22);
if (x_38 == 0)
{
return x_22;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_22, 0);
x_40 = lean_ctor_get(x_22, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_22);
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_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_2);
x_42 = !lean_is_exclusive(x_19);
if (x_42 == 0)
{
return x_19;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_19, 0);
x_44 = lean_ctor_get(x_19, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_19);
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;
}
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go(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; size_t x_13; size_t x_14; lean_object* x_15; lean_object* x_16;
x_12 = lean_array_get_size(x_3);
x_13 = lean_usize_of_nat(x_12);
lean_dec(x_12);
x_14 = 0;
x_15 = lean_box(0);
x_16 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___spec__1(x_1, x_2, x_3, x_13, x_14, x_15, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_16) == 0)
{
uint8_t x_17;
x_17 = !lean_is_exclusive(x_16);
if (x_17 == 0)
{
lean_object* x_18;
x_18 = lean_ctor_get(x_16, 0);
lean_dec(x_18);
lean_ctor_set(x_16, 0, x_15);
return x_16;
}
else
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_16, 1);
lean_inc(x_19);
lean_dec(x_16);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_15);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_20, 0);
x_38 = lean_ctor_get(x_20, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_20);
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_12);
lean_dec(x_11);
lean_dec(x_10);
uint8_t x_21;
x_21 = !lean_is_exclusive(x_16);
if (x_21 == 0)
{
return x_16;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = lean_ctor_get(x_16, 0);
x_23 = lean_ctor_get(x_16, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_16);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
return x_24;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___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, lean_object* x_13, lean_object* x_14) {
_start:
{
size_t x_15; size_t x_16; lean_object* x_17;
x_15 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_16 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_17 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___spec__1(x_1, x_2, x_3, x_15, x_16, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_2);
lean_dec(x_3);
lean_dec(x_1);
x_40 = !lean_is_exclusive(x_17);
if (x_40 == 0)
{
return x_17;
}
else
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go___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_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_17, 0);
x_42 = lean_ctor_get(x_17, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_17);
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_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_2);
lean_object* x_12;
x_12 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go(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_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_44 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_44, 0, x_6);
lean_ctor_set(x_44, 1, x_13);
return x_44;
}
return x_12;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields(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; uint8_t x_13;
x_11 = lean_array_get_size(x_3);
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_nat_dec_lt(x_12, x_11);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15;
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_st_ref_get(x_9, x_10);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___closed__1;
x_14 = lean_st_mk_ref(x_13, x_12);
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_9);
x_17 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_go(x_1, x_2, x_3, x_15, x_4, x_5, x_6, x_7, x_8, x_9, 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, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_st_ref_get(x_9, x_18);
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_2);
lean_dec(x_1);
x_14 = l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___closed__1;
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_10);
return x_15;
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = lean_st_ref_get(x_15, x_20);
lean_dec(x_15);
x_22 = !lean_is_exclusive(x_21);
if (x_22 == 0)
{
return x_21;
}
else
{
uint8_t x_16;
x_16 = lean_nat_dec_le(x_11, x_11);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_11);
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_2);
lean_dec(x_1);
x_17 = l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___closed__1;
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_10);
return x_18;
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_21, 0);
x_24 = lean_ctor_get(x_21, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
else
{
size_t x_19; size_t x_20; lean_object* x_21; lean_object* x_22;
x_19 = 0;
x_20 = lean_usize_of_nat(x_11);
lean_dec(x_11);
x_21 = l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___closed__1;
x_22 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(x_1, x_2, x_3, x_19, x_20, x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_5);
return x_22;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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, lean_object* x_13) {
_start:
uint8_t x_26;
lean_dec(x_15);
lean_dec(x_9);
x_26 = !lean_is_exclusive(x_17);
if (x_26 == 0)
{
size_t x_14; size_t x_15; lean_object* x_16;
x_14 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_15 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_16 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(x_1, x_2, x_3, x_14, x_15, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_8);
lean_dec(x_3);
return x_16;
return x_17;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_17, 0);
x_28 = lean_ctor_get(x_17, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_17);
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_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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) {
@ -18775,7 +18857,9 @@ _start:
{
lean_object* x_11;
x_11 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
return x_11;
}
}
@ -18830,6 +18914,7 @@ lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_14);
x_17 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields(x_15, x_14, x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_12);
lean_dec(x_15);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
@ -18892,7 +18977,6 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
return x_29;
}
}
@ -18903,7 +18987,6 @@ 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_30 = !lean_is_exclusive(x_10);
@ -18932,6 +19015,7 @@ _start:
{
lean_object* x_10;
x_10 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse(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_1);
return x_10;
}
@ -20209,7 +20293,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_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__1;
x_2 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_registerStructure___spec__2___closed__1;
x_3 = lean_unsigned_to_nat(710u);
x_3 = lean_unsigned_to_nat(714u);
x_4 = lean_unsigned_to_nat(21u);
x_5 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_registerStructure___spec__2___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -20230,7 +20314,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_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__1;
x_2 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_registerStructure___spec__2___closed__1;
x_3 = lean_unsigned_to_nat(709u);
x_3 = lean_unsigned_to_nat(713u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_registerStructure___spec__2___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -22333,7 +22417,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_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__1;
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent_copyFields___spec__1___closed__1;
x_3 = lean_unsigned_to_nat(757u);
x_3 = lean_unsigned_to_nat(761u);
x_4 = lean_unsigned_to_nat(79u);
x_5 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -22642,7 +22726,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_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__1;
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent_copyFields___spec__1___closed__1;
x_3 = lean_unsigned_to_nat(748u);
x_3 = lean_unsigned_to_nat(752u);
x_4 = lean_unsigned_to_nat(72u);
x_5 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -23258,7 +23342,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_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__1;
x_2 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent___closed__1;
x_3 = lean_unsigned_to_nat(742u);
x_3 = lean_unsigned_to_nat(746u);
x_4 = lean_unsigned_to_nat(68u);
x_5 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_copyNewFieldsFrom_mkCompositeField___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25925,7 +26009,6 @@ lean_object* x_73;
lean_inc(x_15);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
x_73 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse(x_18, x_8, x_10, x_11, x_12, x_13, x_59, x_15, x_19);
if (lean_obj_tag(x_73) == 0)
@ -29018,7 +29101,7 @@ x_15 = l_Lean_Elab_Command_elabStructure___lambda__7(x_1, x_2, x_3, x_13, x_5, x
return x_15;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10848_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10951_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -29727,7 +29810,7 @@ l_Lean_Elab_Command_elabStructure___closed__12 = _init_l_Lean_Elab_Command_elabS
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__12);
l_Lean_Elab_Command_elabStructure___closed__13 = _init_l_Lean_Elab_Command_elabStructure___closed__13();
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__13);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10848_(lean_io_mk_world());
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_10951_(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));

1222
stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c generated
View file

File diff suppressed because it is too large Load diff

369
stage0/stdlib/Lean/Level.c generated
View file

@ -70,6 +70,7 @@ LEAN_EXPORT uint8_t l_Lean_Level_hasMVar(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_hasMVarEx___boxed(lean_object*);
static lean_object* l_Lean_Level_mkData___closed__2;
lean_object* l_Lean_Name_reprPrec(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Level_geq_go(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Level_isEquiv(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_instBEqLevel;
@ -108,6 +109,7 @@ uint8_t lean_usize_dec_lt(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Level_instToFormatLevel(lean_object*);
LEAN_EXPORT lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_geq___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Level_updateMax_x21___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Level_0__Lean_Level_isAlreadyNormalizedCheap___boxed(lean_object*);
static lean_object* l_Lean_Level_PP_Result_format___closed__6;
@ -141,6 +143,7 @@ lean_object* l_ReaderT_bind___at_Lean_Unhygienic_instMonadQuotationUnhygienic___
LEAN_EXPORT lean_object* l_Lean_Level_isParam___boxed(lean_object*);
static lean_object* l_Lean_Level_PP_toResult___closed__2;
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Level_geq(lean_object*, lean_object*);
LEAN_EXPORT uint32_t lean_level_depth(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_isIMax___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_insert___at_Lean_Level_collectMVars___spec__1(lean_object*, lean_object*, lean_object*);
@ -172,6 +175,7 @@ LEAN_EXPORT lean_object* l_Lean_Level_depth___boxed(lean_object*);
LEAN_EXPORT lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_toNat(lean_object*);
static lean_object* l___private_Lean_Level_0__Lean_reprMVarId____x40_Lean_Level___hyg_512____closed__5;
LEAN_EXPORT lean_object* l_Lean_Level_geq_go___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Level_normLtAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedMVarIdMap(lean_object*);
@ -6983,6 +6987,371 @@ return x_2;
}
}
}
LEAN_EXPORT uint8_t l_Lean_Level_geq_go(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = lean_level_eq(x_1, x_2);
if (x_3 == 0)
{
switch (lean_obj_tag(x_1)) {
case 1:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_4;
x_4 = 1;
return x_4;
}
case 1:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_2, 0);
x_1 = x_5;
x_2 = x_6;
goto _start;
}
case 4:
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = l_Lean_Level_getLevelOffset(x_2);
x_9 = l_Lean_Level_getLevelOffset(x_1);
x_10 = lean_level_eq(x_9, x_8);
lean_dec(x_9);
if (x_10 == 0)
{
uint8_t x_11;
x_11 = l_Lean_Level_isZero(x_8);
lean_dec(x_8);
if (x_11 == 0)
{
uint8_t x_12;
x_12 = 0;
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_Level_getOffsetAux(x_2, x_13);
x_15 = l_Lean_Level_getOffsetAux(x_1, x_13);
x_16 = lean_nat_dec_le(x_14, x_15);
lean_dec(x_15);
lean_dec(x_14);
return x_16;
}
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20;
lean_dec(x_8);
x_17 = lean_unsigned_to_nat(0u);
x_18 = l_Lean_Level_getOffsetAux(x_2, x_17);
x_19 = l_Lean_Level_getOffsetAux(x_1, x_17);
x_20 = lean_nat_dec_le(x_18, x_19);
lean_dec(x_19);
lean_dec(x_18);
return x_20;
}
}
case 5:
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = l_Lean_Level_getLevelOffset(x_2);
x_22 = l_Lean_Level_getLevelOffset(x_1);
x_23 = lean_level_eq(x_22, x_21);
lean_dec(x_22);
if (x_23 == 0)
{
uint8_t x_24;
x_24 = l_Lean_Level_isZero(x_21);
lean_dec(x_21);
if (x_24 == 0)
{
uint8_t x_25;
x_25 = 0;
return x_25;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_26 = lean_unsigned_to_nat(0u);
x_27 = l_Lean_Level_getOffsetAux(x_2, x_26);
x_28 = l_Lean_Level_getOffsetAux(x_1, x_26);
x_29 = lean_nat_dec_le(x_27, x_28);
lean_dec(x_28);
lean_dec(x_27);
return x_29;
}
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
lean_dec(x_21);
x_30 = lean_unsigned_to_nat(0u);
x_31 = l_Lean_Level_getOffsetAux(x_2, x_30);
x_32 = l_Lean_Level_getOffsetAux(x_1, x_30);
x_33 = lean_nat_dec_le(x_31, x_32);
lean_dec(x_32);
lean_dec(x_31);
return x_33;
}
}
default:
{
lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_34 = lean_ctor_get(x_2, 0);
x_35 = lean_ctor_get(x_2, 1);
x_36 = l_Lean_Level_geq_go(x_1, x_34);
if (x_36 == 0)
{
uint8_t x_37;
x_37 = 0;
return x_37;
}
else
{
x_2 = x_35;
goto _start;
}
}
}
}
case 2:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_39;
x_39 = 1;
return x_39;
}
case 2:
{
lean_object* x_40; lean_object* x_41; uint8_t x_42;
x_40 = lean_ctor_get(x_2, 0);
x_41 = lean_ctor_get(x_2, 1);
x_42 = l_Lean_Level_geq_go(x_1, x_40);
if (x_42 == 0)
{
uint8_t x_43;
x_43 = 0;
return x_43;
}
else
{
x_2 = x_41;
goto _start;
}
}
default:
{
lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_45 = lean_ctor_get(x_1, 0);
x_46 = lean_ctor_get(x_1, 1);
x_47 = l_Lean_Level_geq_go(x_45, x_2);
if (x_47 == 0)
{
x_1 = x_46;
goto _start;
}
else
{
uint8_t x_49;
x_49 = 1;
return x_49;
}
}
}
}
case 3:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_50;
x_50 = 1;
return x_50;
}
case 2:
{
lean_object* x_51; lean_object* x_52; uint8_t x_53;
x_51 = lean_ctor_get(x_2, 0);
x_52 = lean_ctor_get(x_2, 1);
x_53 = l_Lean_Level_geq_go(x_1, x_51);
if (x_53 == 0)
{
uint8_t x_54;
x_54 = 0;
return x_54;
}
else
{
x_2 = x_52;
goto _start;
}
}
case 3:
{
lean_object* x_56; lean_object* x_57; uint8_t x_58;
x_56 = lean_ctor_get(x_2, 0);
x_57 = lean_ctor_get(x_2, 1);
x_58 = l_Lean_Level_geq_go(x_1, x_56);
if (x_58 == 0)
{
uint8_t x_59;
x_59 = 0;
return x_59;
}
else
{
x_2 = x_57;
goto _start;
}
}
default:
{
lean_object* x_61;
x_61 = lean_ctor_get(x_1, 1);
x_1 = x_61;
goto _start;
}
}
}
default:
{
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_63;
x_63 = 1;
return x_63;
}
case 2:
{
lean_object* x_64; lean_object* x_65; uint8_t x_66;
x_64 = lean_ctor_get(x_2, 0);
x_65 = lean_ctor_get(x_2, 1);
x_66 = l_Lean_Level_geq_go(x_1, x_64);
if (x_66 == 0)
{
uint8_t x_67;
x_67 = 0;
return x_67;
}
else
{
x_2 = x_65;
goto _start;
}
}
case 3:
{
lean_object* x_69; lean_object* x_70; uint8_t x_71;
x_69 = lean_ctor_get(x_2, 0);
x_70 = lean_ctor_get(x_2, 1);
x_71 = l_Lean_Level_geq_go(x_1, x_69);
if (x_71 == 0)
{
uint8_t x_72;
x_72 = 0;
return x_72;
}
else
{
x_2 = x_70;
goto _start;
}
}
default:
{
lean_object* x_74; lean_object* x_75; uint8_t x_76;
x_74 = l_Lean_Level_getLevelOffset(x_2);
x_75 = l_Lean_Level_getLevelOffset(x_1);
x_76 = lean_level_eq(x_75, x_74);
lean_dec(x_75);
if (x_76 == 0)
{
uint8_t x_77;
x_77 = l_Lean_Level_isZero(x_74);
lean_dec(x_74);
if (x_77 == 0)
{
uint8_t x_78;
x_78 = 0;
return x_78;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81; uint8_t x_82;
x_79 = lean_unsigned_to_nat(0u);
x_80 = l_Lean_Level_getOffsetAux(x_2, x_79);
x_81 = l_Lean_Level_getOffsetAux(x_1, x_79);
x_82 = lean_nat_dec_le(x_80, x_81);
lean_dec(x_81);
lean_dec(x_80);
return x_82;
}
}
else
{
lean_object* x_83; lean_object* x_84; lean_object* x_85; uint8_t x_86;
lean_dec(x_74);
x_83 = lean_unsigned_to_nat(0u);
x_84 = l_Lean_Level_getOffsetAux(x_2, x_83);
x_85 = l_Lean_Level_getOffsetAux(x_1, x_83);
x_86 = lean_nat_dec_le(x_84, x_85);
lean_dec(x_85);
lean_dec(x_84);
return x_86;
}
}
}
}
}
}
else
{
uint8_t x_87;
x_87 = 1;
return x_87;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Level_geq_go___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Level_geq_go(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_Lean_Level_geq(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Level_normalize(x_1);
x_4 = l_Lean_Level_normalize(x_2);
x_5 = l_Lean_Level_geq_go(x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Level_geq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Level_geq(x_1, x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_RBNode_ins___at_Lean_Level_collectMVars___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

3097
stage0/stdlib/Lean/Meta/PPGoal.c generated
View file

File diff suppressed because it is too large Load diff

590
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Solver.c generated
View file

File diff suppressed because it is too large Load diff

862
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff