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-07-18 23:44:45 -04:00
parent e1fc904786
commit 678cfda909
18 changed files with 3759 additions and 4064 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1061,6 +1061,12 @@ def SepArray.getElems (sa : SepArray sep) : Array Syntax :=
def TSepArray.getElems (sa : TSepArray k sep) : TSyntaxArray k :=
.mk sa.elemsAndSeps.getSepElems
def TSepArray.push (sa : TSepArray k sep) (e : TSyntax k) : TSepArray k sep :=
if sa.elemsAndSeps.isEmpty then
{ elemsAndSeps := #[e] }
else
{ elemsAndSeps := sa.elemsAndSeps.push (mkAtom sep) |>.push e }
/-
We use `CoeTail` here instead of `Coe` to avoid a "loop" when computing `CoeTC`.
The "loop" is interrupted using the maximum instance size threshold, but it is a performance bottleneck.

60
stage0/src/Init/Prelude.lean generated
View file

@ -1844,20 +1844,20 @@ end Name
/-- Source information of tokens. -/
inductive SourceInfo where
| /--
Token from original input with whitespace and position information.
`leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,
it is not at all clear what the preceding token was, especially with backtracking.
-/
Token from original input with whitespace and position information.
`leading` will be inferred after parsing by `Syntax.updateLeading`. During parsing,
it is not at all clear what the preceding token was, especially with backtracking.
-/
original (leading : Substring) (pos : String.Pos) (trailing : Substring) (endPos : String.Pos)
| /--
Synthesized token (e.g. from a quotation) annotated with a span from the original source.
In the delaborator, we "misuse" this constructor to store synthetic positions identifying
subterms.
-/
Synthesized token (e.g. from a quotation) annotated with a span from the original source.
In the delaborator, we "misuse" this constructor to store synthetic positions identifying
subterms.
-/
synthetic (pos : String.Pos) (endPos : String.Pos)
| /--
Synthesized token without position information.
-/
Synthesized token without position information.
-/
protected none
instance : Inhabited SourceInfo := ⟨SourceInfo.none⟩
@ -1882,25 +1882,26 @@ Syntax objects used by the parser, macro expander, delaborator, etc.
inductive Syntax where
| missing : Syntax
| /--
Node in the syntax tree.
Node in the syntax tree.
The `info` field is used by the delaborator
to store the position of the subexpression
corresponding to this node.
The parser sets the `info` field to `none`.
The `info` field is used by the delaborator
to store the position of the subexpression
corresponding to this node.
The parser sets the `info` field to `none`.
(Remark: the `node` constructor
did not have an `info` field in previous versions.
This caused a bug in the interactive widgets,
where the popup for `a + b` was the same as for `a`.
The delaborator used to associate subexpressions
with pretty-printed syntax by setting
the (string) position of the first atom/identifier
to the (expression) position of the subexpression.
For example, both `a` and `a + b`
have the same first identifier,
and so their infos got mixed up.)
-/ node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
(Remark: the `node` constructor
did not have an `info` field in previous versions.
This caused a bug in the interactive widgets,
where the popup for `a + b` was the same as for `a`.
The delaborator used to associate subexpressions
with pretty-printed syntax by setting
the (string) position of the first atom/identifier
to the (expression) position of the subexpression.
For example, both `a` and `a + b`
have the same first identifier,
and so their infos got mixed up.)
-/
node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
| atom (info : SourceInfo) (val : String) : Syntax
| ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax
@ -2144,10 +2145,11 @@ def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
introduced symbol, which results in better error positions than not applying
any position. -/
class MonadQuotation (m : Type → Type) extends MonadRef m where
-- Get the fresh scope of the current macro invocation
/-- Get the fresh scope of the current macro invocation -/
getCurrMacroScope : m MacroScope
getMainModule : m Name
/- Execute action in a new macro invocation context. This transformer should be
/--
Execute action in a new macro invocation context. This transformer should be
used at all places that morally qualify as the beginning of a "macro call",
e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
can also be used internally inside a "macro" if identifiers introduced by

9
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -325,7 +325,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
throwError "invalid syntax node kind '{k}'"
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
let `($[$doc?:docComment]? $attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
| throwUnsupportedSyntax
let cat := catStx.getId.eraseMacroScopes
unless (Parser.isParserCategory (← getEnv) cat) do
@ -344,11 +344,14 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
let (val, lhsPrec?) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat
let declName := mkIdentFrom stx name
let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num)
let attrInstances := attrInstances.getD { elemsAndSeps := #[] }
let attrInstances := attrInstances.push attrInstance
let d ← if let some lhsPrec := lhsPrec? then
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.TrailingParserDescr :=
`($[$doc?:docComment]? @[$attrInstances,*] def $declName:ident : Lean.TrailingParserDescr :=
ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
else
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.ParserDescr :=
`($[$doc?:docComment]? @[$attrInstances,*] def $declName:ident : Lean.ParserDescr :=
ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
trace `Elab fun _ => d
withMacroExpansion stx d <| elabCommand d

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

@ -53,7 +53,7 @@ This can be set to
The difference between implicit `{}` and strict-implicit `⦃⦄` is how
implicit arguments are treated that are *not* followed by explicit arguments.
`{}` arguments are applied eagerly, while `⦃⦄` arguments are left partially applied:
```lean
```lean4
def foo {x : Nat} : Nat := x
def bar ⦃x : Nat⦄ : Nat := x
#check foo -- foo : Nat
@ -72,17 +72,17 @@ inductive BinderInfo where
| /-- Local instance binder annotataion, e.g., `[Decidable α]` -/
instImplicit
| /--
Auxiliary declarations used by Lean when elaborating recursive declarations.
When defining a function such as
```
def f : Nat → Nat
| 0 => 1
| x+1 => (x+1)*f x
```
Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`)
with `BinderInfo` set to `auxDecl`.
This local declaration is later removed by the termination checker.
-/
Auxiliary declarations used by Lean when elaborating recursive declarations.
When defining a function such as
```
def f : Nat → Nat
| 0 => 1
| x+1 => (x+1)*f x
```
Lean adds a local declaration `f : Nat → Nat` to the local context (`LocalContext`)
with `BinderInfo` set to `auxDecl`.
This local declaration is later removed by the termination checker.
-/
auxDecl
deriving Inhabited, BEq, Repr
@ -297,127 +297,127 @@ Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keyword
We considered using «...», but it is too inconvenient to use. -/
inductive Expr where
| /--
Bound variables. The natural number is the "de Bruijn" index
for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
Example, the expression `fun x : Nat => forall y : Nat, x = y`
```lean
.lam `x (.const `Nat [])
(.forall `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero])
(.const `Nat [])) (.bvar 1))
(.bvar 0))
.default)
.default
```
-/
Bound variables. The natural number is the "de Bruijn" index
for the bound variable. See https://en.wikipedia.org/wiki/De_Bruijn_index for additional information.
Example, the expression `fun x : Nat => forall y : Nat, x = y`
```lean
.lam `x (.const `Nat [])
(.forall `y (.const `Nat [])
(.app (.app (.app (.const `Eq [.succ .zero])
(.const `Nat [])) (.bvar 1))
(.bvar 0))
.default)
.default
```
-/
bvar (deBruijnIndex : Nat)
| /--
Free variable. Lean uses the locally nameless approach.
See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
are converted into free variables using a unique identifier, and their user-facing name, type,
value (for `LetE`), and binder annotation are stored in the `LocalContext`.
-/
Free variable. Lean uses the locally nameless approach.
See https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf for additional details.
When "visiting" the body of a binding expression (`lam`, `forallE`, or `letE`), bound variables
are converted into free variables using a unique identifier, and their user-facing name, type,
value (for `LetE`), and binder annotation are stored in the `LocalContext`.
-/
fvar (fvarId : FVarId)
| /--
Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
Metavariables are used during elaboration, and are not allowed in the kernel,
or in the code generator.
Metavariables are used to represent "holes" in expressions, and goals in the
tactic framework. Metavariable declarations are stored in the `MetavarContext`.
Metavariables are used during elaboration, and are not allowed in the kernel,
or in the code generator.
-/
mvar (mvarId : MVarId)
| /--
`Type u`, `Sort u`, `Prop`. -
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
-/
`Type u`, `Sort u`, `Prop`. -
- `Prop` is represented as `.sort .zero`,
- `Sort u` as ``.sort (.param `u)``, and
- `Type u` as ``.sort (.succ (.param `u))``
-/
sort (u : Level)
| /--
A (universe polymorphic) constant. For example,
`@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
`@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``.
-/
A (universe polymorphic) constant. For example,
`@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
`@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``.
-/
const (declName : Name) (us : List Level)
| /--
Function application. `Nat.succ Nat.zero` is represented as
```lean
.app (.const `Nat.succ []) (.const .zero [])
```
-/
Function application. `Nat.succ Nat.zero` is represented as
```lean4
.app (.const `Nat.succ []) (.const .zero [])
```
-/
app (fn : Expr) (arg : Expr)
| /--
Lambda abstraction (aka anonymous functions).
- `fun x : Nat => x` is represented as
```lean
.lam `x (.const `Nat []) (.bvar 0) .default
```
-/
Lambda abstraction (aka anonymous functions).
- `fun x : Nat => x` is represented as
```lean4
.lam `x (.const `Nat []) (.bvar 0) .default
```
-/
lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
| /--
A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
Examples:
A dependent arrow (aka forall-expression). It is also used to represent non-dependent arrows.
Examples:
- `forall x : Prop, x ∧ x` is represented as
```lean
.forallE `x
(.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
.default
```
- `Nat → Bool` as
```lean
.forallE `a (.const `Nat []) (.const `Bool []) .default
```
-/
- `forall x : Prop, x ∧ x` is represented as
```lean4
.forallE `x
(.sort .zero)
(.app (.app (.const `And []) (.bvar 0)) (.bvar 0))
.default
```
- `Nat → Bool` as
```lean4
.forallE `a (.const `Nat []) (.const `Bool []) .default
```
-/
forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
| /--
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
or not. Given an environment, metavariable context, and local context, we say a let-expression
`let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`.
Here is an example of a dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but
`(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
-/
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
or not. Given an environment, metavariable context, and local context, we say a let-expression
`let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`.
Here is an example of a dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but
`(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
The let-expression `let x : Nat := 2; Nat.succ x` is represented as
```
.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
```
-/
letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
| /--
Natural number and string literal values. They are not really needed, but provide a more
compact representation in memory for these two kinds of literals, and are used to implement
efficient reduction in the elaborator and kernel.
The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
definitionally equal to
```
.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
-/
Natural number and string literal values. They are not really needed, but provide a more
compact representation in memory for these two kinds of literals, and are used to implement
efficient reduction in the elaborator and kernel.
The "raw" natural number `2` can be represented as `.lit (.natVal 2)`. Note that, it is
definitionally equal to
```lean4
.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
-/
lit : Literal → Expr
| /--
Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).
Note that `.mdata data e` is definitionally equal to `e`.
-/
Metadata (aka annotations). We use annotations to provide hints to the pretty-printer,
store references to `Syntax` nodes, position information, and save information for
elaboration procedures (e.g., we use the `inaccessible` annotation during elaboration to
mark `Expr`s that correspond to inaccessible patterns).
Note that `.mdata data e` is definitionally equal to `e`.
-/
mdata (data : MData) (expr : Expr)
| /--
Projection-expressions. They are redundant, but are used to create more compact
terms, speedup reduction, and implement eta for structures.
The type of `struct` must be an structure-like inductive type. That is, it has only one
constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators
check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index
is valid (i.e., it is smaller than the numbef of constructor fields).
When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec`
applications.
Example, given `a : Nat x Bool`, `a.1` is represented as
```
.proj `Prod 0 a
```
-/
Projection-expressions. They are redundant, but are used to create more compact
terms, speedup reduction, and implement eta for structures.
The type of `struct` must be an structure-like inductive type. That is, it has only one
constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators
check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index
is valid (i.e., it is smaller than the numbef of constructor fields).
When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec`
applications.
Example, given `a : Nat x Bool`, `a.1` is represented as
```lean4
.proj `Prod 0 a
```
-/
proj (typeName : Name) (idx : Nat) (struct : Expr)
with
@[computedField, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]

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

@ -69,7 +69,7 @@ def optKind : Parser := optional ("(" >> nonReservedSymbol "kind" >> ":=" >> ide
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := leading_parser Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> optional (Term.«attributes») >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := leading_parser optional docComment >> "syntax " >> ident >> " := " >> many1 syntaxParser
def catBehaviorBoth := leading_parser nonReservedSymbol "both"
def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"

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);
opts = opts.update({"pp", "rawOnError"}, true);
#endif
return opts;

1993
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

189
stage0/stdlib/Lean/Elab/ElabRules.c generated
View file

@ -6358,7 +6358,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabElab___lambda__1___closed__6()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(9u);
x_1 = lean_unsigned_to_nat(10u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
@ -6611,21 +6611,21 @@ lean_ctor_set(x_120, 2, x_119);
if (lean_obj_tag(x_14) == 0)
{
x_121 = x_76;
goto block_173;
goto block_174;
}
else
{
lean_object* x_174; lean_object* x_175;
x_174 = lean_ctor_get(x_14, 0);
lean_inc(x_174);
lean_object* x_175; lean_object* x_176;
x_175 = lean_ctor_get(x_14, 0);
lean_inc(x_175);
lean_dec(x_14);
x_175 = lean_array_push(x_56, x_174);
x_121 = x_175;
goto block_173;
x_176 = lean_array_push(x_56, x_175);
x_121 = x_176;
goto block_174;
}
block_173:
block_174:
{
lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135;
lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136;
x_122 = l_Array_append___rarg(x_76, x_121);
x_123 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_123, 0, x_24);
@ -6634,107 +6634,108 @@ lean_ctor_set(x_123, 2, x_122);
x_124 = l_Lean_Elab_Command_elabElab___lambda__1___closed__6;
lean_inc(x_123);
x_125 = lean_array_push(x_124, x_123);
x_126 = lean_array_push(x_125, x_10);
x_127 = lean_array_push(x_126, x_38);
x_128 = l_Lean_Elab_Command_elabElabRules___lambda__3___closed__2;
x_129 = lean_array_push(x_128, x_123);
x_130 = lean_array_push(x_129, x_84);
x_131 = lean_array_push(x_130, x_85);
x_132 = l_Lean_Elab_Command_elabElabRulesAux___lambda__1___closed__90;
x_133 = lean_array_push(x_131, x_132);
x_134 = lean_array_push(x_133, x_89);
x_126 = l_Lean_Elab_Command_elabElabRulesAux___lambda__1___closed__90;
x_127 = lean_array_push(x_125, x_126);
x_128 = lean_array_push(x_127, x_10);
x_129 = lean_array_push(x_128, x_38);
x_130 = l_Lean_Elab_Command_elabElabRules___lambda__3___closed__2;
x_131 = lean_array_push(x_130, x_123);
x_132 = lean_array_push(x_131, x_84);
x_133 = lean_array_push(x_132, x_85);
x_134 = lean_array_push(x_133, x_126);
x_135 = lean_array_push(x_134, x_89);
if (lean_obj_tag(x_12) == 0)
{
lean_dec(x_87);
lean_dec(x_13);
x_135 = x_76;
goto block_166;
x_136 = x_76;
goto block_167;
}
else
{
lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172;
x_167 = lean_ctor_get(x_12, 0);
lean_inc(x_167);
lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173;
x_168 = lean_ctor_get(x_12, 0);
lean_inc(x_168);
lean_dec(x_12);
x_168 = l_Lean_Elab_Command_elabElab___lambda__1___closed__10;
x_169 = l_Lean_Name_str___override(x_13, x_168);
x_170 = lean_array_push(x_87, x_167);
x_171 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_171, 0, x_24);
lean_ctor_set(x_171, 1, x_169);
lean_ctor_set(x_171, 2, x_170);
x_172 = lean_array_push(x_56, x_171);
x_135 = x_172;
goto block_166;
x_169 = l_Lean_Elab_Command_elabElab___lambda__1___closed__10;
x_170 = l_Lean_Name_str___override(x_13, x_169);
x_171 = lean_array_push(x_87, x_168);
x_172 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_172, 0, x_24);
lean_ctor_set(x_172, 1, x_170);
lean_ctor_set(x_172, 2, x_171);
x_173 = lean_array_push(x_56, x_172);
x_136 = x_173;
goto block_167;
}
block_166:
block_167:
{
lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145;
x_136 = l_Array_append___rarg(x_76, x_135);
x_137 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_137, 0, x_24);
lean_ctor_set(x_137, 1, x_58);
lean_ctor_set(x_137, 2, x_136);
x_138 = lean_array_push(x_127, x_137);
x_139 = lean_array_push(x_138, x_59);
x_140 = lean_array_push(x_139, x_72);
x_141 = lean_array_push(x_140, x_78);
x_142 = lean_array_push(x_141, x_80);
x_143 = lean_array_push(x_142, x_7);
x_144 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_144, 0, x_24);
lean_ctor_set(x_144, 1, x_37);
lean_ctor_set(x_144, 2, x_143);
x_145 = lean_array_push(x_86, x_144);
lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146;
x_137 = l_Array_append___rarg(x_76, x_136);
x_138 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_138, 0, x_24);
lean_ctor_set(x_138, 1, x_58);
lean_ctor_set(x_138, 2, x_137);
x_139 = lean_array_push(x_129, x_138);
x_140 = lean_array_push(x_139, x_59);
x_141 = lean_array_push(x_140, x_72);
x_142 = lean_array_push(x_141, x_78);
x_143 = lean_array_push(x_142, x_80);
x_144 = lean_array_push(x_143, x_7);
x_145 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_145, 0, x_24);
lean_ctor_set(x_145, 1, x_37);
lean_ctor_set(x_145, 2, x_144);
x_146 = lean_array_push(x_86, x_145);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152;
lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153;
lean_dec(x_30);
x_146 = l_Lean_Elab_Command_elabElabRulesAux___lambda__1___closed__59;
x_147 = lean_array_push(x_134, x_146);
x_148 = lean_array_push(x_147, x_120);
x_149 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_149, 0, x_24);
lean_ctor_set(x_149, 1, x_82);
lean_ctor_set(x_149, 2, x_148);
x_150 = lean_array_push(x_145, x_149);
x_151 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_151, 0, x_24);
lean_ctor_set(x_151, 1, x_58);
lean_ctor_set(x_151, 2, x_150);
x_152 = l_Lean_Elab_Command_elabCommand(x_151, x_16, x_17, x_35);
return x_152;
x_147 = l_Lean_Elab_Command_elabElabRulesAux___lambda__1___closed__59;
x_148 = lean_array_push(x_135, x_147);
x_149 = lean_array_push(x_148, x_120);
x_150 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_150, 0, x_24);
lean_ctor_set(x_150, 1, x_82);
lean_ctor_set(x_150, 2, x_149);
x_151 = lean_array_push(x_146, x_150);
x_152 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_152, 0, x_24);
lean_ctor_set(x_152, 1, x_58);
lean_ctor_set(x_152, 2, x_151);
x_153 = l_Lean_Elab_Command_elabCommand(x_152, x_16, x_17, x_35);
return x_153;
}
else
{
lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165;
x_153 = lean_ctor_get(x_11, 0);
lean_inc(x_153);
lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166;
x_154 = lean_ctor_get(x_11, 0);
lean_inc(x_154);
lean_dec(x_11);
x_154 = l_Lean_Elab_Command_elabElabRules___lambda__3___closed__3;
x_155 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_155, 0, x_30);
lean_ctor_set(x_155, 1, x_154);
x_156 = lean_array_push(x_86, x_155);
x_157 = lean_array_push(x_156, x_153);
x_158 = l_Array_append___rarg(x_76, x_157);
x_159 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_159, 0, x_24);
lean_ctor_set(x_159, 1, x_58);
lean_ctor_set(x_159, 2, x_158);
x_160 = lean_array_push(x_134, x_159);
x_161 = lean_array_push(x_160, x_120);
x_162 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_162, 0, x_24);
lean_ctor_set(x_162, 1, x_82);
lean_ctor_set(x_162, 2, x_161);
x_163 = lean_array_push(x_145, x_162);
x_164 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_164, 0, x_24);
lean_ctor_set(x_164, 1, x_58);
lean_ctor_set(x_164, 2, x_163);
x_165 = l_Lean_Elab_Command_elabCommand(x_164, x_16, x_17, x_35);
return x_165;
x_155 = l_Lean_Elab_Command_elabElabRules___lambda__3___closed__3;
x_156 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_156, 0, x_30);
lean_ctor_set(x_156, 1, x_155);
x_157 = lean_array_push(x_86, x_156);
x_158 = lean_array_push(x_157, x_154);
x_159 = l_Array_append___rarg(x_76, x_158);
x_160 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_160, 0, x_24);
lean_ctor_set(x_160, 1, x_58);
lean_ctor_set(x_160, 2, x_159);
x_161 = lean_array_push(x_135, x_160);
x_162 = lean_array_push(x_161, x_120);
x_163 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_163, 0, x_24);
lean_ctor_set(x_163, 1, x_82);
lean_ctor_set(x_163, 2, x_162);
x_164 = lean_array_push(x_146, x_163);
x_165 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_165, 0, x_24);
lean_ctor_set(x_165, 1, x_58);
lean_ctor_set(x_165, 2, x_164);
x_166 = l_Lean_Elab_Command_elabCommand(x_165, x_16, x_17, x_35);
return x_166;
}
}
}

134
stage0/stdlib/Lean/Elab/Macro.c generated
View file

@ -525,7 +525,7 @@ static lean_object* _init_l_Lean_Elab_Command_elabMacro___lambda__2___closed__27
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(9u);
x_1 = lean_unsigned_to_nat(10u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
@ -667,16 +667,16 @@ lean_ctor_set(x_267, 1, x_266);
if (lean_obj_tag(x_7) == 0)
{
x_268 = x_263;
goto block_304;
goto block_306;
}
else
{
lean_object* x_305; lean_object* x_306;
x_305 = lean_ctor_get(x_7, 0);
lean_inc(x_305);
x_306 = lean_array_push(x_243, x_305);
x_268 = x_306;
goto block_304;
lean_object* x_307; lean_object* x_308;
x_307 = lean_ctor_get(x_7, 0);
lean_inc(x_307);
x_308 = lean_array_push(x_243, x_307);
x_268 = x_308;
goto block_306;
}
block_215:
{
@ -1088,9 +1088,9 @@ return x_214;
}
}
}
block_304:
block_306:
{
lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274;
lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276;
x_269 = l_Array_append___rarg(x_263, x_268);
x_270 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_270, 0, x_24);
@ -1098,81 +1098,83 @@ lean_ctor_set(x_270, 1, x_245);
lean_ctor_set(x_270, 2, x_269);
x_271 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__27;
x_272 = lean_array_push(x_271, x_270);
x_273 = lean_array_push(x_272, x_11);
x_273 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__3;
x_274 = lean_array_push(x_272, x_273);
x_275 = lean_array_push(x_274, x_11);
if (lean_obj_tag(x_225) == 0)
{
x_274 = x_217;
goto block_302;
x_276 = x_217;
goto block_304;
}
else
{
lean_object* x_303;
lean_object* x_305;
lean_dec(x_217);
x_303 = lean_ctor_get(x_225, 0);
lean_inc(x_303);
x_305 = lean_ctor_get(x_225, 0);
lean_inc(x_305);
lean_dec(x_225);
x_274 = x_303;
goto block_302;
x_276 = x_305;
goto block_304;
}
block_302:
block_304:
{
lean_object* x_275; lean_object* x_276;
x_275 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_275, 0, x_274);
lean_ctor_set(x_275, 1, x_223);
x_276 = lean_array_push(x_273, x_275);
lean_object* x_277; lean_object* x_278;
x_277 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_277, 0, x_276);
lean_ctor_set(x_277, 1, x_223);
x_278 = lean_array_push(x_275, x_277);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284;
lean_object* x_279; 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;
lean_dec(x_14);
x_277 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__17;
x_278 = lean_array_push(x_276, x_277);
x_279 = lean_array_push(x_278, x_246);
x_280 = lean_array_push(x_279, x_259);
x_281 = lean_array_push(x_280, x_265);
x_282 = lean_array_push(x_281, x_267);
x_283 = lean_array_push(x_282, x_13);
x_284 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_284, 0, x_24);
lean_ctor_set(x_284, 1, x_224);
lean_ctor_set(x_284, 2, x_283);
x_29 = x_284;
x_279 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__17;
x_280 = lean_array_push(x_278, x_279);
x_281 = lean_array_push(x_280, x_246);
x_282 = lean_array_push(x_281, x_259);
x_283 = lean_array_push(x_282, x_265);
x_284 = lean_array_push(x_283, x_267);
x_285 = lean_array_push(x_284, x_13);
x_286 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_286, 0, x_24);
lean_ctor_set(x_286, 1, x_224);
lean_ctor_set(x_286, 2, x_285);
x_29 = x_286;
x_30 = x_222;
goto block_215;
}
else
{
lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301;
x_285 = lean_ctor_get(x_12, 0);
lean_inc(x_285);
lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303;
x_287 = lean_ctor_get(x_12, 0);
lean_inc(x_287);
lean_dec(x_12);
x_286 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__28;
x_287 = l_Lean_Name_str___override(x_14, x_286);
x_288 = l_Lean_Elab_Command_elabMacro___lambda__1___closed__1;
x_288 = l_Lean_Elab_Command_elabMacro___lambda__2___closed__28;
x_289 = l_Lean_Name_str___override(x_14, x_288);
x_290 = l_Lean_Elab_Command_elabMacro___lambda__1___closed__1;
lean_inc(x_267);
x_289 = lean_array_push(x_288, x_267);
x_290 = lean_array_push(x_289, x_285);
x_291 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_291, 0, x_24);
lean_ctor_set(x_291, 1, x_287);
lean_ctor_set(x_291, 2, x_290);
x_292 = lean_array_push(x_243, x_291);
x_293 = l_Array_append___rarg(x_263, x_292);
x_294 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_294, 0, x_24);
lean_ctor_set(x_294, 1, x_245);
lean_ctor_set(x_294, 2, x_293);
x_295 = lean_array_push(x_276, x_294);
x_296 = lean_array_push(x_295, x_246);
x_297 = lean_array_push(x_296, x_259);
x_298 = lean_array_push(x_297, x_265);
x_299 = lean_array_push(x_298, x_267);
x_300 = lean_array_push(x_299, x_13);
x_301 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_301, 0, x_24);
lean_ctor_set(x_301, 1, x_224);
lean_ctor_set(x_301, 2, x_300);
x_29 = x_301;
x_291 = lean_array_push(x_290, x_267);
x_292 = lean_array_push(x_291, x_287);
x_293 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_293, 0, x_24);
lean_ctor_set(x_293, 1, x_289);
lean_ctor_set(x_293, 2, x_292);
x_294 = lean_array_push(x_243, x_293);
x_295 = l_Array_append___rarg(x_263, x_294);
x_296 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_296, 0, x_24);
lean_ctor_set(x_296, 1, x_245);
lean_ctor_set(x_296, 2, x_295);
x_297 = lean_array_push(x_278, x_296);
x_298 = lean_array_push(x_297, x_246);
x_299 = lean_array_push(x_298, x_259);
x_300 = lean_array_push(x_299, x_265);
x_301 = lean_array_push(x_300, x_267);
x_302 = lean_array_push(x_301, x_13);
x_303 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_303, 0, x_24);
lean_ctor_set(x_303, 1, x_224);
lean_ctor_set(x_303, 2, x_302);
x_29 = x_303;
x_30 = x_222;
goto block_215;
}

17
stage0/stdlib/Lean/Elab/Notation.c generated
View file

@ -38,6 +38,7 @@ static lean_object* l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNo
static lean_object* l_Lean_Elab_Command_mkSimpleDelab___lambda__1___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36;
static lean_object* l_Lean_Elab_Command_mkSimpleDelab___lambda__1___closed__53;
static lean_object* l_Lean_Elab_Command_mkSimpleDelab___lambda__1___closed__42;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_expandNotation___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -5901,7 +5902,7 @@ static lean_object* _init_l___private_Lean_Elab_Notation_0__Lean_Elab_Command_ex
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(9u);
x_1 = lean_unsigned_to_nat(10u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
@ -5916,6 +5917,16 @@ x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__35;
x_2 = l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__3;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2(lean_object* x_1, size_t x_2, size_t 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:
{
@ -6069,7 +6080,7 @@ x_170 = l_Lean_Elab_Command_expandNotationItemIntoSyntaxItem___lambda__1___close
x_171 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_171, 0, x_127);
lean_ctor_set(x_171, 1, x_170);
x_172 = l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__35;
x_172 = l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36;
lean_inc(x_7);
x_173 = lean_array_push(x_172, x_7);
x_174 = lean_array_push(x_173, x_130);
@ -7496,6 +7507,8 @@ l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__
lean_mark_persistent(l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__34);
l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__35 = _init_l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__35();
lean_mark_persistent(l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__35);
l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36 = _init_l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36();
lean_mark_persistent(l___private_Lean_Elab_Notation_0__Lean_Elab_Command_expandNotationAux___lambda__2___closed__36);
l_Lean_Elab_Command_expandNotation___closed__1 = _init_l_Lean_Elab_Command_expandNotation___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_expandNotation___closed__1);
l_Lean_Elab_Command_expandNotation___closed__2 = _init_l_Lean_Elab_Command_expandNotation___closed__2();

3288
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -239,7 +239,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallMetaBoundedTelescope(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadEnvMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___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_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_setInlineAttribute___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1392,7 +1392,7 @@ x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_3, x_6);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_3, x_6);
if (x_9 == 0)
{
uint8_t x_10;
@ -7240,7 +7240,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 0;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -7256,7 +7256,7 @@ lean_dec(x_6);
x_15 = 0;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
@ -7290,7 +7290,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 2;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -7306,7 +7306,7 @@ lean_dec(x_6);
x_15 = 2;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);

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

@ -232,7 +232,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAss
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass___spec__2___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processConstApprox_defaultCase___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process___closed__2;
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Lean_markUsedAssignment___at_Lean_Meta_CheckAssignment_checkApp___spec__3(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqEtaStruct_go___spec__1___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqArgsFirstPass(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -72024,7 +72024,7 @@ x_11 = lean_ctor_get(x_8, 1);
x_12 = 3;
x_13 = lean_unbox(x_10);
lean_dec(x_10);
x_14 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_13, x_12);
x_14 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_13, x_12);
if (x_14 == 0)
{
uint8_t x_15; lean_object* x_16;
@ -72059,7 +72059,7 @@ lean_dec(x_8);
x_21 = 3;
x_22 = lean_unbox(x_19);
lean_dec(x_19);
x_23 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_22, x_21);
x_23 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_22, x_21);
if (x_23 == 0)
{
uint8_t x_24; lean_object* x_25; lean_object* x_26;

6
stage0/stdlib/Lean/Meta/GetConst.c generated
View file

@ -21,7 +21,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConstNoEx_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isReducible___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConst_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(uint8_t, uint8_t);
lean_object* l_Lean_ConstantInfo_name(lean_object*);
LEAN_EXPORT lean_object* l_Lean_getReducibilityStatus___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -315,7 +315,7 @@ x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
lean_dec(x_38);
x_40 = 3;
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_6, x_40);
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_6, x_40);
if (x_41 == 0)
{
uint8_t x_42; lean_object* x_43;
@ -360,7 +360,7 @@ x_51 = lean_ctor_get(x_49, 0);
lean_inc(x_51);
lean_dec(x_49);
x_52 = 3;
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_6, x_52);
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_6, x_52);
if (x_53 == 0)
{
uint8_t x_54; lean_object* x_55; lean_object* x_56;

8
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -132,7 +132,7 @@ size_t lean_usize_shift_right(size_t, size_t);
static lean_object* l_Lean_Meta_reduceNative_x3f___closed__14;
LEAN_EXPORT lean_object* l_Lean_Meta_smartUnfoldingMatch_x3f(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_toCtorIfLit___closed__16;
static lean_object* l_Lean_Meta_canUnfoldAtMatcher___closed__10;
uint8_t lean_usize_dec_lt(size_t, size_t);
@ -10112,7 +10112,7 @@ lean_inc(x_9);
lean_dec(x_7);
x_10 = 2;
x_11 = lean_unbox(x_8);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_11, x_10);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_11, x_10);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
@ -19916,7 +19916,7 @@ x_10 = lean_ctor_get(x_7, 1);
x_11 = 3;
x_12 = lean_unbox(x_9);
lean_dec(x_9);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_12, x_11);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_12, x_11);
if (x_13 == 0)
{
lean_object* x_14;
@ -19947,7 +19947,7 @@ lean_dec(x_7);
x_18 = 3;
x_19 = lean_unbox(x_16);
lean_dec(x_16);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9875_(x_19, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_9921_(x_19, x_18);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;

462
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff

915
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff