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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-01 18:42:41 -08:00
parent c476954eef
commit c2ea02b7c4
25 changed files with 3535 additions and 3324 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
stage0/src/Init/Coe.lean generated
View file

@ -187,3 +187,15 @@ instance [CoeTC α β] [Append β] : HAppend α β β where
instance [CoeTC α β] [Append β] : HAppend β α β where
hAppend a b := Append.append a b
instance [CoeTC α β] [OrElse β] : HOrElse α β β where
hOrElse a b := OrElse.orElse a b
instance [CoeTC α β] [OrElse β] : HOrElse β α β where
hOrElse a b := OrElse.orElse a b
instance [CoeTC α β] [AndThen β] : HAndThen α β β where
hAndThen a b := AndThen.andThen a b
instance [CoeTC α β] [AndThen β] : HAndThen β α β where
hAndThen a b := AndThen.andThen a b

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

@ -46,8 +46,8 @@ notation:max "!" b:40 => not b
infixl:65 " ++ " => HAppend.hAppend
infixr:67 " :: " => List.cons
infixr:2 " <|> " => OrElse.orElse
infixr:60 " >> " => AndThen.andThen
infixr:2 " <|> " => HOrElse.hOrElse
infixr:60 " >> " => HAndThen.hAndThen
infixl:55 " >>= " => Bind.bind
infixl:60 " <*> " => Seq.seq
infixl:60 " <* " => SeqLeft.seqLeft

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

@ -378,6 +378,12 @@ class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
class HAppend (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hAppend : α → β → γ
class HOrElse (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hOrElse : α → β → γ
class HAndThen (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hAndThen : α → β → γ
class Add (α : Type u) where
add : α → α → α
@ -436,6 +442,14 @@ instance [Pow α] : HPow α α α where
instance [Append α] : HAppend α α α where
hAppend a b := Append.append a b
@[defaultInstance 1]
instance [OrElse α] : HOrElse α α α where
hOrElse a b := OrElse.orElse a b
@[defaultInstance 1]
instance [AndThen α] : HAndThen α α α where
hAndThen a b := AndThen.andThen a b
open HAdd (hAdd)
open HMul (hMul)
open HPow (hPow)

8
stage0/src/Lean/Parser/Command.lean generated
View file

@ -45,10 +45,10 @@ def «constant» := parser! "constant " >> declId >> declSig >> optional d
def «instance» := parser! "instance " >> optional declId >> declSig >> declVal
def «axiom» := parser! "axiom " >> declId >> declSig
def «example» := parser! "example " >> declSig >> declVal
def inferMod := parser! atomic ("{" >> "}")
def inferMod := parser! atomic (symbol "{" >> "}")
def ctor := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
def classInductive := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor
def classInductive := parser! atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor
def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
@ -60,7 +60,7 @@ def classTk := parser! "class "
def «extends» := parser! " extends " >> sepBy1 termParser ", "
def «structure» := parser!
(structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType
>> optional ((" := " <|> " where ") >> optional structCtor >> structFields)
>> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
@[builtinCommandParser] def declaration := parser!
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)

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

@ -24,7 +24,7 @@ def doSeqBracketed := parser! "{" >> withoutPosition (many1 doSeqItem) >> ppLine
def doSeq := doSeqBracketed <|> doSeqIndent
def notFollowedByRedefinedTermToken :=
notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> "try") "token at 'do' element"
notFollowedBy ("if" <|> "match" <|> "let" <|> "have" <|> "do" <|> "dbgTrace!" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try") "token at 'do' element"
@[builtinDoElemParser] def doLet := parser! "let " >> optional "mut " >> letDecl

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

@ -52,8 +52,8 @@ def optSemicolon (p : Parser) : Parser := ppDedent $ optional ";" >> ppLine >> p
@[builtinTermParser] def hole := parser! "_"
@[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole)
@[builtinTermParser] def «sorry» := parser! "sorry"
@[builtinTermParser] def cdot := parser! "·" <|> "."
@[builtinTermParser] def emptyC := parser! "∅" <|> ("{" >> "}")
@[builtinTermParser] def cdot := parser! symbol "·" <|> "."
@[builtinTermParser] def emptyC := parser! "∅" <|> (symbol "{" >> "}")
def typeAscription := parser! " : " >> termParser
def tupleTail := parser! ", " >> sepBy1 termParser ", "
def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@ -80,7 +80,7 @@ def optType : Parser := optional typeSpec
@[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
def binderIdent : Parser := ident <|> hole
def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
def binderTactic := parser! atomic (" := " >> " by ") >> Tactic.tacticSeq
def binderTactic := parser! atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
def binderDefault := parser! " := " >> termParser
def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
@ -122,7 +122,7 @@ def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space b
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser
def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
def funImplicitBinder := atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
def funSimpleBinder := atomic (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
-- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation

4
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -105,8 +105,8 @@ def delabAppExplicit : Delab := do
(do
let fn ← getExpr
let stx ← if fn.isConst then delabConst else delab
let paramKinds ← liftM $ getParamKinds fn <|> pure #[]
let stx ← if paramKinds.any (fun k => match k with | ParamKind.explicit => false | _ => true) then `(@$stx) else pure stx
let paramKinds ← liftM <| getParamKinds fn <|> pure #[]
let stx ← if paramKinds.any (fun k => match k with | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx
pure (stx, #[]))
(fun ⟨fnStx, argStxs⟩ => do
let argStx ← delab

76
stage0/stdlib/Init/Coe.c generated
View file

@ -28,6 +28,7 @@ lean_object* l_coeD___rarg(lean_object*);
lean_object* l_coeOfTCOfTail(lean_object*, lean_object*, lean_object*);
lean_object* l_instHMul__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_instHOrElse__2(lean_object*, lean_object*);
lean_object* l_instHSub__1(lean_object*, lean_object*);
lean_object* l_instHDiv__1(lean_object*, lean_object*);
lean_object* l_coeTC___rarg(lean_object*, lean_object*);
@ -50,6 +51,8 @@ lean_object* l_instHSub__1___rarg(lean_object*, lean_object*, lean_object*, lean
extern lean_object* l_rawNatLit___closed__4;
lean_object* l_instHMul__2(lean_object*, lean_object*);
lean_object* l_coeOfHeadOfTC___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instHAndThen__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instHAndThen__2(lean_object*, lean_object*);
lean_object* l_decPropToBool___rarg___boxed(lean_object*);
lean_object* l_coeSort___rarg(lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
@ -67,6 +70,7 @@ lean_object* l_liftCoeM___rarg___lambda__1(lean_object*, lean_object*, lean_obje
lean_object* l_coeOfHeadOfTC(lean_object*, lean_object*, lean_object*);
lean_object* l_coeOfTCOfTail___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_Coe___hyg_176____closed__1;
lean_object* l_instHOrElse__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___kind_term____x40_Init_Coe___hyg_141____closed__3;
lean_object* l_instHSub__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_coe___boxed(lean_object*, lean_object*, lean_object*);
@ -74,6 +78,7 @@ lean_object* l___kind_term____x40_Init_Coe___hyg_141____closed__6;
lean_object* l_instHMod__1(lean_object*, lean_object*);
lean_object* l_subtypeCoe___rarg___boxed(lean_object*);
lean_object* l_coeOfHead(lean_object*, lean_object*);
lean_object* l_instHOrElse__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedSourceInfo___closed__1;
lean_object* l_optionCoe___rarg(lean_object*);
lean_object* l_instHAppend__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -112,6 +117,7 @@ extern lean_object* l_Lean_Name_hasMacroScopes___closed__1;
lean_object* l_coeId(lean_object*);
lean_object* l_subtypeCoe___rarg(lean_object*);
lean_object* l_coeFun___rarg(lean_object*, lean_object*);
lean_object* l_instHAndThen__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_coeB(lean_object*, lean_object*);
lean_object* l_subtypeCoe(lean_object*, lean_object*);
@ -132,11 +138,13 @@ lean_object* l_unexpand____x40_Init_Coe___hyg_141____closed__1;
lean_object* l_coeId___rarg(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_intro___closed__14;
lean_object* l_coeId___rarg___boxed(lean_object*);
lean_object* l_instHAndThen__1(lean_object*, lean_object*);
lean_object* l_instCoeTail(lean_object*, lean_object*);
lean_object* l_coeD___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_Coe___hyg_176____closed__3;
lean_object* l_instHAdd__2(lean_object*, lean_object*);
lean_object* l_instHDiv__2(lean_object*, lean_object*);
lean_object* l_instHOrElse__1(lean_object*, lean_object*);
lean_object* l_instHAppend__1(lean_object*, lean_object*);
lean_object* l_decPropToBool(lean_object*);
lean_object* l_coeOfHeafOfTCOfTail(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1282,6 +1290,74 @@ x_3 = lean_alloc_closure((void*)(l_instHAppend__2___rarg), 4, 0);
return x_3;
}
}
lean_object* l_instHOrElse__1___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;
x_5 = lean_apply_1(x_1, x_3);
x_6 = lean_apply_2(x_2, x_5, x_4);
return x_6;
}
}
lean_object* l_instHOrElse__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instHOrElse__1___rarg), 4, 0);
return x_3;
}
}
lean_object* l_instHOrElse__2___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;
x_5 = lean_apply_1(x_1, x_4);
x_6 = lean_apply_2(x_2, x_3, x_5);
return x_6;
}
}
lean_object* l_instHOrElse__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instHOrElse__2___rarg), 4, 0);
return x_3;
}
}
lean_object* l_instHAndThen__1___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;
x_5 = lean_apply_1(x_1, x_3);
x_6 = lean_apply_2(x_2, x_5, x_4);
return x_6;
}
}
lean_object* l_instHAndThen__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instHAndThen__1___rarg), 4, 0);
return x_3;
}
}
lean_object* l_instHAndThen__2___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;
x_5 = lean_apply_1(x_1, x_4);
x_6 = lean_apply_2(x_2, x_3, x_5);
return x_6;
}
}
lean_object* l_instHAndThen__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instHAndThen__2___rarg), 4, 0);
return x_3;
}
}
lean_object* initialize_Init_Core(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Coe(lean_object* w) {

26
stage0/stdlib/Init/Control/Basic.c generated
View file

@ -730,24 +730,24 @@ lean_object* l_optional___rarg(lean_object* x_1, lean_object* x_2, lean_object*
_start:
{
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;
x_4 = lean_ctor_get(x_1, 2);
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_1, 0);
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_optional___rarg___closed__1;
x_9 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_8, x_3);
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_box(0);
x_12 = lean_apply_2(x_10, lean_box(0), x_11);
x_13 = lean_apply_3(x_4, lean_box(0), x_9, x_12);
x_7 = l_optional___rarg___closed__1;
x_8 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_7, x_3);
x_9 = lean_ctor_get(x_4, 1);
lean_inc(x_9);
lean_dec(x_4);
x_10 = lean_box(0);
x_11 = lean_apply_2(x_9, lean_box(0), x_10);
x_12 = lean_ctor_get(x_1, 2);
lean_inc(x_12);
lean_dec(x_1);
x_13 = lean_apply_3(x_12, lean_box(0), x_8, x_11);
return x_13;
}
}

24
stage0/stdlib/Init/Control/Reader.c generated
View file

@ -38,13 +38,13 @@ lean_object* l_ReaderT_orElse___rarg(lean_object* x_1, lean_object* x_2, lean_ob
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_1, 2);
lean_inc(x_5);
lean_dec(x_1);
lean_inc(x_4);
x_6 = lean_apply_1(x_2, x_4);
x_7 = lean_apply_1(x_3, x_4);
x_8 = lean_apply_3(x_5, lean_box(0), x_6, x_7);
x_5 = lean_apply_1(x_2, x_4);
x_6 = lean_apply_1(x_3, x_4);
x_7 = lean_ctor_get(x_1, 2);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_apply_3(x_7, lean_box(0), x_5, x_6);
return x_8;
}
}
@ -99,13 +99,13 @@ lean_object* l_ReaderT_instAlternativeReaderT___rarg___lambda__2(lean_object* x_
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_1, 2);
lean_inc(x_6);
lean_dec(x_1);
lean_inc(x_5);
x_7 = lean_apply_1(x_3, x_5);
x_8 = lean_apply_1(x_4, x_5);
x_9 = lean_apply_3(x_6, lean_box(0), x_7, x_8);
x_6 = lean_apply_1(x_3, x_5);
x_7 = lean_apply_1(x_4, x_5);
x_8 = lean_ctor_get(x_1, 2);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_apply_3(x_8, lean_box(0), x_6, x_7);
return x_9;
}
}

12
stage0/stdlib/Init/Control/State.c generated
View file

@ -487,13 +487,13 @@ lean_object* l_StateT_orElse___rarg(lean_object* x_1, lean_object* x_2, lean_obj
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_1, 2);
lean_inc(x_6);
lean_dec(x_1);
lean_inc(x_5);
x_7 = lean_apply_1(x_3, x_5);
x_8 = lean_apply_1(x_4, x_5);
x_9 = lean_apply_3(x_6, lean_box(0), x_7, x_8);
x_6 = lean_apply_1(x_3, x_5);
x_7 = lean_apply_1(x_4, x_5);
x_8 = lean_ctor_get(x_1, 2);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_apply_3(x_8, lean_box(0), x_6, x_7);
return x_9;
}
}

12
stage0/stdlib/Init/Data/List/Control.c generated
View file

@ -1030,12 +1030,14 @@ lean_inc(x_9);
x_10 = lean_ctor_get(x_6, 1);
lean_inc(x_10);
lean_dec(x_6);
x_11 = lean_ctor_get(x_2, 2);
lean_inc(x_11);
lean_inc(x_5);
x_12 = lean_apply_1(x_5, x_9);
x_13 = l_List_firstM___rarg(x_1, x_2, lean_box(0), lean_box(0), x_5, x_10);
x_14 = lean_apply_3(x_11, lean_box(0), x_12, x_13);
x_11 = lean_apply_1(x_5, x_9);
lean_inc(x_2);
x_12 = l_List_firstM___rarg(x_1, x_2, lean_box(0), lean_box(0), x_5, x_10);
x_13 = lean_ctor_get(x_2, 2);
lean_inc(x_13);
lean_dec(x_2);
x_14 = lean_apply_3(x_13, lean_box(0), x_11, x_12);
return x_14;
}
}

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

@ -11409,7 +11409,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_8955____closed__1
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("OrElse.orElse");
x_1 = lean_mk_string("HOrElse.hOrElse");
return x_1;
}
}
@ -11440,7 +11440,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_8955____closed__4
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("OrElse");
x_1 = lean_mk_string("HOrElse");
return x_1;
}
}
@ -11458,7 +11458,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_8955____closed__6
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("orElse");
x_1 = lean_mk_string("hOrElse");
return x_1;
}
}
@ -11769,7 +11769,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_9266____closed__1
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("AndThen.andThen");
x_1 = lean_mk_string("HAndThen.hAndThen");
return x_1;
}
}
@ -11800,7 +11800,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_9266____closed__4
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("AndThen");
x_1 = lean_mk_string("HAndThen");
return x_1;
}
}
@ -11818,7 +11818,7 @@ static lean_object* _init_l_myMacro____x40_Init_Notation___hyg_9266____closed__6
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("andThen");
x_1 = lean_mk_string("hAndThen");
return x_1;
}
}

36
stage0/stdlib/Init/Prelude.c generated
View file

@ -215,6 +215,7 @@ lean_object* l_Applicative_map___default___rarg(lean_object*, lean_object*, lean
lean_object* l_EStateM_orElse_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Monad_seqLeft___default___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_maxRecDepthErrorMessage___closed__1;
lean_object* l_instHOrElse(lean_object*);
lean_object* l_Lean_Name_instAppendName___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_get___boxed(lean_object*, lean_object*, lean_object*);
@ -764,6 +765,7 @@ lean_object* l_id(lean_object*);
uint8_t l_instDecidableEqBool(uint8_t, uint8_t);
lean_object* l___private_Init_Prelude_0__Lean_assembleParts___closed__1;
lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*);
lean_object* l_instHOrElse___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_extractMainModule_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_dite___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_String_utf8ByteSize___boxed(lean_object*);
@ -804,6 +806,7 @@ uint8_t l_UInt32_decLe(uint32_t, uint32_t);
uint8_t l_instDecidableOr___rarg(uint8_t, uint8_t);
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Prelude_0__Lean_extractImported_match__1(lean_object*);
lean_object* l_instHAndThen(lean_object*);
lean_object* l_instOfNatNat___boxed(lean_object*);
lean_object* l_Lean_MonadQuotation_addMacroScope(lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
@ -829,6 +832,7 @@ lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux___closed__1;
lean_object* l___private_Init_Prelude_0__Lean_extractImported_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getOp(lean_object*, lean_object*);
lean_object* l_Array_mk___boxed(lean_object*, lean_object*);
lean_object* l_instHAndThen___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_modifyGetThe___rarg(lean_object*, lean_object*);
lean_object* l_modify___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHeadInfo_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -2216,6 +2220,38 @@ x_2 = lean_alloc_closure((void*)(l_instHAppend___rarg), 3, 0);
return x_2;
}
}
lean_object* l_instHOrElse___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_apply_2(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_instHOrElse(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_instHOrElse___rarg), 3, 0);
return x_2;
}
}
lean_object* l_instHAndThen___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_apply_2(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_instHAndThen(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_instHAndThen___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Nat_add___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{

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

@ -58,6 +58,7 @@ extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
lean_object* l_Lean_Elab_Term_elabSubst_match__1___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandAssert___closed__1;
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31;
lean_object* l_Lean_Elab_Term_expandHave___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_getPropToDecide___closed__3;
lean_object* l_Lean_Elab_Term_getDeclName_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -72,7 +73,6 @@ lean_object* l_Lean_Elab_Term_elabPanic___closed__3;
lean_object* l_Lean_Elab_Term_expandAssert___closed__23;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__11;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_mkNativeReflAuxDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__8;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -157,6 +157,7 @@ lean_object* l_Lean_Elab_Term_expandDbgTrace___closed__2;
lean_object* l_Lean_Elab_Term_expandShow___closed__1;
lean_object* l_Lean_Elab_Term_expandSorry___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30;
lean_object* l___regBuiltin_Lean_Elab_Term_expandShow___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -200,6 +201,7 @@ lean_object* l_Lean_Elab_Term_elabParen___closed__4;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__3;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__10;
lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32;
uint8_t l_Lean_Occurrences_beq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandAssert___closed__24;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -352,6 +354,7 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserM
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_kabstract___at_Lean_Elab_Term_elabSubst___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___regBuiltin_Lean_Elab_Term_elabByTactic___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabClosedTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandAssert___closed__6;
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__2;
@ -400,6 +403,7 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_main_module(lean_object*);
extern lean_object* l_Lean_instQuoteBool___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__5;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__14;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__15;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_54____closed__6;
@ -496,7 +500,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_getPropToDe
extern lean_object* l_Lean_Syntax_expandInterpolatedStr___lambda__1___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__2;
lean_object* l_Lean_Elab_Term_elabBorrowed___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_8955____closed__3;
lean_object* l_Lean_Elab_Term_mkPairs___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__7;
lean_object* l_Lean_Meta_inferType___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -580,6 +583,7 @@ uint8_t l_Lean_Expr_hasFVar(lean_object*);
lean_object* l_Lean_Elab_getRefPosition___at_Lean_Elab_Term_elabPanic___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_expandCDot_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33;
lean_object* l___regBuiltin_Lean_Elab_Term_elabBorrowed___closed__1;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabClosedTerm___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Term_elabTParserMacro___closed__1;
@ -603,6 +607,7 @@ lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__4;
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__2;
extern lean_object* l_Lean_Meta_throwLetTypeMismatchMessage___rarg___closed__8;
lean_object* l___regBuiltin_Lean_Elab_Term_expandUnreachable___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34;
lean_object* l_Lean_Syntax_reprint(lean_object*);
extern lean_object* l___kind_term____x40_Init_Notation___hyg_8298____closed__1;
lean_object* l_Lean_Elab_Term_expandCDot_x3f_match__1___rarg(lean_object*, lean_object*);
@ -3694,51 +3699,27 @@ return x_3;
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("OrElse.orElse");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__14;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__14;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.Parser.mkAntiquot");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__14;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__17;
x_3 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3746,11 +3727,29 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("OrElse");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__17;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkAntiquot");
x_1 = lean_mk_string("orElse");
return x_1;
}
}
@ -3758,7 +3757,7 @@ static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Ter
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_54____closed__4;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__19;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
@ -3791,19 +3790,27 @@ return x_3;
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__5;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string("Lean.Parser.mkAntiquot");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__24() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__23;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__5;
x_1 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__23;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__23;
x_3 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__24;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -3811,7 +3818,72 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25() {
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkAntiquot");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_54____closed__4;
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__5;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__5;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30;
x_4 = lean_alloc_ctor(0, 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___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -3821,7 +3893,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26() {
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -3833,12 +3905,12 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27() {
static lean_object* _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26;
x_2 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -3946,24 +4018,24 @@ if (x_51 == 0)
{
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; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89;
x_52 = lean_ctor_get(x_50, 0);
x_53 = l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
x_53 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
lean_inc(x_48);
lean_inc(x_52);
x_54 = l_Lean_addMacroScope(x_52, x_53, x_48);
x_55 = l_myMacro____x40_Init_Notation___hyg_8955____closed__3;
x_56 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15;
x_55 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_56 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_57 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_57, 0, x_22);
lean_ctor_set(x_57, 1, x_55);
lean_ctor_set(x_57, 2, x_54);
lean_ctor_set(x_57, 3, x_56);
x_58 = lean_array_push(x_36, x_57);
x_59 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
x_59 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
lean_inc(x_48);
lean_inc(x_52);
x_60 = l_Lean_addMacroScope(x_52, x_59, x_48);
x_61 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
x_62 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_61 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_62 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
x_63 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_63, 0, x_22);
lean_ctor_set(x_63, 1, x_61);
@ -4022,24 +4094,24 @@ x_91 = lean_ctor_get(x_50, 1);
lean_inc(x_91);
lean_inc(x_90);
lean_dec(x_50);
x_92 = l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
x_92 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
lean_inc(x_48);
lean_inc(x_90);
x_93 = l_Lean_addMacroScope(x_90, x_92, x_48);
x_94 = l_myMacro____x40_Init_Notation___hyg_8955____closed__3;
x_95 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15;
x_94 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_95 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_96 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_96, 0, x_22);
lean_ctor_set(x_96, 1, x_94);
lean_ctor_set(x_96, 2, x_93);
lean_ctor_set(x_96, 3, x_95);
x_97 = lean_array_push(x_36, x_96);
x_98 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
x_98 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
lean_inc(x_48);
lean_inc(x_90);
x_99 = l_Lean_addMacroScope(x_90, x_98, x_48);
x_100 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
x_101 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_100 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_101 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
x_102 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_102, 0, x_22);
lean_ctor_set(x_102, 1, x_100);
@ -4109,24 +4181,24 @@ if (x_134 == 0)
{
lean_object* x_135; 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; 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_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; lean_object* 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; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182;
x_135 = lean_ctor_get(x_133, 0);
x_136 = l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
x_136 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
lean_inc(x_131);
lean_inc(x_135);
x_137 = l_Lean_addMacroScope(x_135, x_136, x_131);
x_138 = l_myMacro____x40_Init_Notation___hyg_8955____closed__3;
x_139 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15;
x_138 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_139 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_140 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_140, 0, x_22);
lean_ctor_set(x_140, 1, x_138);
lean_ctor_set(x_140, 2, x_137);
lean_ctor_set(x_140, 3, x_139);
x_141 = lean_array_push(x_36, x_140);
x_142 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
x_142 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
lean_inc(x_131);
lean_inc(x_135);
x_143 = l_Lean_addMacroScope(x_135, x_142, x_131);
x_144 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
x_145 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_144 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_145 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
x_146 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_146, 0, x_22);
lean_ctor_set(x_146, 1, x_144);
@ -4134,10 +4206,10 @@ lean_ctor_set(x_146, 2, x_143);
lean_ctor_set(x_146, 3, x_145);
x_147 = lean_array_push(x_36, x_146);
x_148 = lean_array_push(x_36, x_23);
x_149 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_149 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32;
x_150 = l_Lean_addMacroScope(x_135, x_149, x_131);
x_151 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__24;
x_152 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
x_151 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31;
x_152 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34;
x_153 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_153, 0, x_22);
lean_ctor_set(x_153, 1, x_151);
@ -4203,24 +4275,24 @@ x_184 = lean_ctor_get(x_133, 1);
lean_inc(x_184);
lean_inc(x_183);
lean_dec(x_133);
x_185 = l_myMacro____x40_Init_Notation___hyg_8955____closed__7;
x_185 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
lean_inc(x_131);
lean_inc(x_183);
x_186 = l_Lean_addMacroScope(x_183, x_185, x_131);
x_187 = l_myMacro____x40_Init_Notation___hyg_8955____closed__3;
x_188 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__15;
x_187 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__16;
x_188 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_189 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_189, 0, x_22);
lean_ctor_set(x_189, 1, x_187);
lean_ctor_set(x_189, 2, x_186);
lean_ctor_set(x_189, 3, x_188);
x_190 = lean_array_push(x_36, x_189);
x_191 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__20;
x_191 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
lean_inc(x_131);
lean_inc(x_183);
x_192 = l_Lean_addMacroScope(x_183, x_191, x_131);
x_193 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__18;
x_194 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__22;
x_193 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_194 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29;
x_195 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_195, 0, x_22);
lean_ctor_set(x_195, 1, x_193);
@ -4228,10 +4300,10 @@ lean_ctor_set(x_195, 2, x_192);
lean_ctor_set(x_195, 3, x_194);
x_196 = lean_array_push(x_36, x_195);
x_197 = lean_array_push(x_36, x_23);
x_198 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
x_198 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32;
x_199 = l_Lean_addMacroScope(x_183, x_198, x_131);
x_200 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__24;
x_201 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27;
x_200 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31;
x_201 = l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34;
x_202 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_202, 0, x_22);
lean_ctor_set(x_202, 1, x_200);
@ -14777,6 +14849,20 @@ l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___clo
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__26);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__27);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__29);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__30);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__31);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__32);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__33);
l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34 = _init_l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34();
lean_mark_persistent(l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__34);
l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__1);
l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2 = _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__2();

6
stage0/stdlib/Lean/Elab/PreDefinition/Structural.c generated
View file

@ -404,7 +404,7 @@ lean_object* l_Lean_Meta_decLevel___at___private_Lean_Elab_PreDefinition_Structu
lean_object* l_Lean_Meta_MatcherApp_toExpr(lean_object*);
lean_object* l_Std_PersistentArray_forIn___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadIndexDep_x3f_match__1(lean_object*);
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4151_(lean_object*);
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4163_(lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_replaceRecApps_loop___spec__14(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadParamDep_x3f___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadIndexDep_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -16011,7 +16011,7 @@ return x_42;
}
}
}
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4151_(lean_object* x_1) {
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4163_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -16237,7 +16237,7 @@ l_Lean_Elab_Structural_structuralRecursion___closed__3 = _init_l_Lean_Elab_Struc
lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__3);
l_Lean_Elab_Structural_structuralRecursion___closed__4 = _init_l_Lean_Elab_Structural_structuralRecursion___closed__4();
lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__4);
res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4151_(lean_io_mk_world());
res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_4163_(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));

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

@ -369,7 +369,7 @@ extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3438____closed_
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkExpectedTypeHintImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_hasTypeMsg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4127_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4129_(lean_object*);
lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkProjectionImp___lambda__1___closed__3;
@ -13221,7 +13221,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_mkArbitrary___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4127_(lean_object* x_1) {
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4129_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -13473,7 +13473,7 @@ l_Lean_Meta_mkArbitrary___rarg___closed__1 = _init_l_Lean_Meta_mkArbitrary___rar
lean_mark_persistent(l_Lean_Meta_mkArbitrary___rarg___closed__1);
l_Lean_Meta_mkArbitrary___rarg___closed__2 = _init_l_Lean_Meta_mkArbitrary___rarg___closed__2();
lean_mark_persistent(l_Lean_Meta_mkArbitrary___rarg___closed__2);
res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4127_(lean_io_mk_world());
res = l_Lean_Meta_initFn____x40_Lean_Meta_AppBuilder___hyg_4129_(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));

6
stage0/stdlib/Lean/Meta/Tactic/Cases.c generated
View file

@ -241,7 +241,7 @@ size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_mkCasesContext_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_hasIndepIndices___spec__43(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t);
lean_object* l_Lean_Meta_generalizeTargets___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2419_(lean_object*);
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2421_(lean_object*);
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_Tactic_Cases_0__Lean_Meta_Cases_hasIndepIndices___spec__15(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t);
lean_object* l_Lean_Meta_Cases_unifyEqs_substEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -13871,7 +13871,7 @@ x_11 = l_Lean_Meta_cases(x_1, x_2, x_3, x_10, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2419_(lean_object* x_1) {
lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2421_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -13967,7 +13967,7 @@ l_Lean_Meta_Cases_cases___lambda__1___closed__6 = _init_l_Lean_Meta_Cases_cases_
lean_mark_persistent(l_Lean_Meta_Cases_cases___lambda__1___closed__6);
l_Lean_Meta_Cases_cases___closed__1 = _init_l_Lean_Meta_Cases_cases___closed__1();
lean_mark_persistent(l_Lean_Meta_Cases_cases___closed__1);
res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2419_(lean_io_mk_world());
res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Cases___hyg_2421_(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));

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

File diff suppressed because it is too large Load diff

1120
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

32
stage0/stdlib/Lean/Parser/Level.c generated
View file

@ -346,23 +346,13 @@ static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__5() {
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -374,24 +364,34 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__6() {
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__5;
x_2 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
x_2 = l_Lean_Parser_Level_paren___elambda__1___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Level_paren___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__3;
x_2 = l_Lean_Parser_Level_paren___elambda__1___closed__6;
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__6;
x_2 = l_Lean_Parser_Level_paren___elambda__1___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);

110
stage0/stdlib/Lean/Parser/Module.c generated
View file

@ -27,7 +27,6 @@ extern lean_object* l_Lean_Syntax_strLitToAtom___closed__3;
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Parser_Module_0__Lean_Parser_testModuleParserAux_loop___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_updateTokens___closed__2;
lean_object* l___private_Lean_Parser_Module_0__Lean_Parser_testModuleParserAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__7;
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserContext(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_prelude_parenthesizer___closed__2;
@ -40,7 +39,6 @@ lean_object* l_Std_PersistentArray_forM___at___private_Lean_Parser_Module_0__Lea
lean_object* l_Lean_Parser_Module_module_formatter___closed__9;
lean_object* l_Lean_Parser_parseModule(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nullKind;
extern lean_object* l_Lean_Parser_Term_quot___closed__2;
lean_object* l___private_Lean_Parser_Module_0__Lean_Parser_mkEOI(lean_object*);
lean_object* l_Lean_Parser_topLevelCommandParserFn___closed__3;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -139,6 +137,7 @@ lean_object* l_Lean_Parser_Module_import_parenthesizer___closed__1;
lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__11;
lean_object* l_Lean_Parser_Module_module_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Command_exit___elambda__1___closed__2;
@ -268,6 +267,7 @@ extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__6;
lean_object* l_Lean_Parser_Module_prelude___closed__2;
lean_object* l_Lean_Parser_topLevelCommandParserFn___closed__1;
extern lean_object* l_Lean_Parser_Term_quot___closed__1;
lean_object* l_Lean_Parser_Module_module_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_import_formatter___closed__2;
lean_object* l_Lean_Parser_parseModuleAux_parse_match__1___rarg(lean_object*, lean_object*);
@ -571,7 +571,7 @@ static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__4()
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("import ");
x_1 = lean_mk_string("runtime");
return x_1;
}
}
@ -597,45 +597,18 @@ return x_2;
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("runtime");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__7;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__8;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__9;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__6;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optionalFn), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__11() {
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__10;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__7;
x_2 = l_Lean_Parser_ident___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -643,12 +616,39 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("import ");
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__9;
x_2 = l_String_trim(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__10;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__6;
x_2 = l_Lean_Parser_Module_import___elambda__1___closed__11;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__11;
x_2 = l_Lean_Parser_Module_import___elambda__1___closed__8;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -705,38 +705,38 @@ static lean_object* _init_l_Lean_Parser_Module_import___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__8;
x_2 = l_Lean_Parser_symbolInfo(x_1);
x_1 = l_Lean_Parser_Module_import___closed__1;
x_2 = l_Lean_Parser_optionaInfo(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___closed__2;
x_2 = l_Lean_Parser_optionaInfo(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_ident;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Module_import___closed__2;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_ident;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Module_import___closed__3;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__10;
x_2 = l_Lean_Parser_symbolInfo(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Parser_Module_import___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_import___closed__1;
x_2 = l_Lean_Parser_Module_import___closed__4;
x_1 = l_Lean_Parser_Module_import___closed__4;
x_2 = l_Lean_Parser_Module_import___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
@ -1135,7 +1135,7 @@ static lean_object* _init_l_Lean_Parser_Module_import_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__4;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__9;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -1145,7 +1145,7 @@ static lean_object* _init_l_Lean_Parser_Module_import_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__7;
x_1 = l_Lean_Parser_Module_import___elambda__1___closed__4;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -1787,7 +1787,7 @@ static lean_object* _init_l_Lean_Parser_Module_module___elambda__1___closed__3()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_quot___elambda__1___closed__7;
x_1 = l_Lean_Parser_Term_quot___elambda__1___closed__4;
x_2 = l_Lean_Parser_Module_module___elambda__1___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -1867,7 +1867,7 @@ static lean_object* _init_l_Lean_Parser_Module_module___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_quot___closed__2;
x_1 = l_Lean_Parser_Term_quot___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Module_module___closed__1;
@ -2675,7 +2675,7 @@ lean_object* l_Lean_Parser_topLevelCommandParserFn(lean_object* x_1, lean_object
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6;
x_3 = l_Lean_Parser_Term_quot___elambda__1___closed__7;
x_3 = l_Lean_Parser_Term_quot___elambda__1___closed__4;
x_4 = l_Lean_Parser_topLevelCommandParserFn___closed__4;
x_5 = 0;
x_6 = l_Lean_Parser_orelseFnCore(x_3, x_4, x_5, x_1, x_2);

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated
View file

@ -311,7 +311,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_mkDelabAttribute___closed__10;
extern lean_object* l_Lean_Expr_ctorName___closed__6;
lean_object* l_Lean_Level_quote___closed__5;
lean_object* l_Lean_PrettyPrinter_Delaborator_withAppFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2059_(lean_object*);
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2061_(lean_object*);
lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_574____closed__1;
lean_object* lean_mk_syntax_ident(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
@ -10447,7 +10447,7 @@ goto block_39;
}
}
}
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2059_(lean_object* x_1) {
lean_object* l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2061_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -10713,7 +10713,7 @@ l_Lean_PrettyPrinter_delab___closed__5 = _init_l_Lean_PrettyPrinter_delab___clos
lean_mark_persistent(l_Lean_PrettyPrinter_delab___closed__5);
l_Lean_PrettyPrinter_delab___closed__6 = _init_l_Lean_PrettyPrinter_delab___closed__6();
lean_mark_persistent(l_Lean_PrettyPrinter_delab___closed__6);
res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2059_(lean_io_mk_world());
res = l_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter_Delaborator_Basic___hyg_2061_(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));