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-01-17 17:14:46 -08:00
parent 0f217eb4c1
commit db9bb8dd1b
2 changed files with 40 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -170,6 +170,9 @@ structure Subtype {α : Sort u} (p : α → Prop) where
/-- Auxiliary Declaration used to implement the notation (a : α) -/
@[reducible] def typedExpr (α : Sort u) (a : α) : α := a
-- TODO: delete
@[reducible] def namedPatternOld {α : Sort u} (x a : α) : α := a
/-- Auxiliary Declaration used to implement the named patterns `x@p`
-- TODO: add proof for `x = a`
-/

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

@ -285,11 +285,13 @@ LEAN_EXPORT lean_object* l_ReaderT_read___at_Lean_PrettyPrinter_instMonadQuotati
LEAN_EXPORT lean_object* l_withTheReader___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_UInt16_val___boxed(lean_object*);
static lean_object* l_Lean_Macro_instInhabitedMethods___closed__2;
LEAN_EXPORT lean_object* l_namedPatternOld___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_strLitKind;
static uint32_t l_Char_utf8Size___closed__5;
LEAN_EXPORT lean_object* l_EStateM_modifyGet___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_mixHash___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_instDecidableEqList___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_namedPatternOld___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_EStateM_map(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Syntax_getId___boxed(lean_object*);
LEAN_EXPORT lean_object* l_instMonadWithReaderOfReaderT___rarg(lean_object*, lean_object*, lean_object*);
@ -384,6 +386,7 @@ LEAN_EXPORT lean_object* l_Lean_Macro_throwErrorAt___rarg(lean_object*, lean_obj
LEAN_EXPORT lean_object* l_False_elim___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instInhabitedList(lean_object*);
LEAN_EXPORT lean_object* l_instMonadWithReaderOf(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_namedPatternOld___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_getOp(lean_object*);
static lean_object* l_Lean_numLitKind___closed__2;
LEAN_EXPORT lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
@ -445,6 +448,7 @@ LEAN_EXPORT lean_object* l_List_length(lean_object*);
static uint32_t l_instInhabitedUInt32___closed__1;
LEAN_EXPORT lean_object* l_ReaderT_instMonadLiftReaderT___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instMonadFunctorT___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_namedPatternOld(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ite___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_namedPattern___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_or(uint8_t, uint8_t);
@ -1055,6 +1059,39 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_namedPatternOld___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
LEAN_EXPORT lean_object* l_namedPatternOld(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_namedPatternOld___rarg___boxed), 1, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l_namedPatternOld___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_namedPatternOld___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_namedPatternOld___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_namedPatternOld(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_namedPattern___rarg(lean_object* x_1) {
_start:
{