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-03-14 11:16:48 -07:00
parent 6f9583987d
commit cef43ceb1f
2 changed files with 66 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
stage0/src/Init/Core.lean
View file

@ -1707,6 +1707,35 @@ Quot.lift f (fun a b _ => Subsingleton.elim _ _) s
instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩
namespace Lean
/- Kernel reduction hints -/
/--
When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
The kernel will produce an error message if `c` is not a constant.
This feature is useful for performing proofs by reflection.
Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
`Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.
Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using
external type checkers (e.g., Trepplein) that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your developement using external checkers. -/
def reduceBool (b : Bool) : Bool := b
/--
Similar to `Lean.reduceBool` for closed `Nat` terms.
Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
def reduceNat (n : Nat) : Nat := n
end Lean
/- Classical reasoning support -/
namespace Classical

37
stage0/stdlib/Init/Core.c
View file

@ -23,6 +23,7 @@ lean_object* l_Subtype_sizeof(lean_object*);
lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
lean_object* l_Prod_DecidableEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_reduceBool(uint8_t);
lean_object* l_inline(lean_object*);
lean_object* l_Quotient_lift_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_condEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -42,6 +43,7 @@ lean_object* l_Quotient_lift___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Squash_mk___rarg___boxed(lean_object*);
lean_object* l_Nat_HasOne;
lean_object* l_idRhs___rarg___boxed(lean_object*);
lean_object* l_Lean_reduceBool___boxed(lean_object*);
lean_object* l_arbitrary___rarg___boxed(lean_object*);
lean_object* l_absurd(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_sizeof___main(lean_object*);
@ -129,6 +131,7 @@ lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*);
lean_object* l_setoidHasEquiv(lean_object*, lean_object*);
lean_object* l_PUnit_sizeof(lean_object*);
lean_object* l_Iff_Decidable(lean_object*, lean_object*);
lean_object* l_Lean_reduceNat(lean_object*);
lean_object* l_Nat_HasSizeof;
lean_object* l_Squash_lift___rarg(lean_object*, lean_object*);
lean_object* l_Ne_Decidable___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -270,6 +273,7 @@ lean_object* l_Option_HasSizeof(lean_object*);
lean_object* l_PSum_HasSizeof(lean_object*, lean_object*);
lean_object* l_Function_const(lean_object*, lean_object*);
lean_object* l_PUnit_Inhabited;
lean_object* l_Lean_reduceNat___boxed(lean_object*);
lean_object* l_Sum_HasSizeof(lean_object*, lean_object*);
lean_object* l_Option_sizeof___rarg(lean_object*, lean_object*);
lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3619,6 +3623,39 @@ x_4 = lean_alloc_closure((void*)(l_Squash_lift___rarg), 2, 0);
return x_4;
}
}
uint8_t l_Lean_reduceBool(uint8_t x_1) {
_start:
{
return x_1;
}
}
lean_object* l_Lean_reduceBool___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_reduceBool(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_reduceNat(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
lean_object* l_Lean_reduceNat___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_reduceNat(x_1);
lean_dec(x_1);
return x_2;
}
}
static bool _G_initialized = false;
lean_object* initialize_Init_Core(lean_object* w) {
lean_object * res;