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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-30 18:40:14 -07:00
parent 0a018f2369
commit cf350e556d
3 changed files with 4179 additions and 3586 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -387,6 +387,10 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
let pat := stx[2]
let pat ← collect pat
`(_root_.namedPattern $id $pat)
else if k == ``Lean.Parser.Term.binop then
let lhs ← collect stx[2]
let rhs ← collect stx[3]
return stx.setArg 2 lhs |>.setArg 3 rhs
else if k == ``Lean.Parser.Term.inaccessible then
return stx
else if k == strLitKind then

7757
stage0/stdlib/Lean/Elab/Match.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -40,11 +40,11 @@ lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpan
lean_object* l_Lean_Elab_Tactic_AuxMatchTermState_cases___default;
size_t l_USize_sub(size_t, size_t);
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9331____closed__1;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTerm_match__1(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9295____closed__1;
lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Tactic_evalIntro___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
@ -1593,7 +1593,7 @@ lean_dec(x_277);
x_316 = lean_ctor_get(x_6, 0);
lean_inc(x_316);
lean_dec(x_6);
x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9295____closed__1;
x_317 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Match___hyg_9331____closed__1;
x_318 = l_Lean_Name_appendIndexAfter(x_317, x_316);
x_319 = l_Lean_Name_append(x_1, x_318);
x_320 = l_Lean_mkIdentFrom(x_30, x_319);