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

fix: mismatch between TheoremVal in Lean and C++ (#4035)

Browse source
This commit is contained in:
Leonardo de Moura 2024-04-30 20:10:20 +02:00 • committed by GitHub
parent 6e731b4370
commit 5c3f6363cc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Declaration.lean
View file

@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
all : List Name := [name]
deriving Inhabited, BEq
@[export lean_mk_theorem_val]
def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
name, levelParams, type, value, all
}
/-- Value for an opaque constant declaration `opaque x : t := e` -/
structure OpaqueVal extends ConstantVal where
value : Expr

8
src/kernel/declaration.cpp
View file

@ -71,8 +71,10 @@ definition_val::definition_val(name const & n, names const & lparams, expr const
definition_safety definition_val::get_safety() const { return static_cast<definition_safety>(lean_definition_val_get_safety(to_obj_arg())); }
theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val):
object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
extern "C" object * lean_mk_theorem_val(object * n, object * lparams, object * type, object * value, object * all);
theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all):
object_ref(lean_mk_theorem_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), all.to_obj_arg())) {
}
extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe, object * all);
@ -206,7 +208,7 @@ declaration mk_definition(environment const & env, name const & n, names const &
}
declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val, names(n))));
}
declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {

7
src/kernel/declaration.h
View file

@ -112,12 +112,13 @@ public:
typedef list_ref<definition_val> definition_vals;
/*
structure theorem_val extends constant_val :=
(value : task expr)
structure TheoremVal extends ConstantVal where
value : Expr
all : List Name := [name]
*/
class theorem_val : public object_ref {
public:
theorem_val(name const & n, names const & lparams, expr const & type, expr const & val);
theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
theorem_val(theorem_val const & other):object_ref(other) {}
theorem_val(theorem_val && other):object_ref(other) {}
theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }