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

feat: add sanity checks

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-01 18:31:28 -08:00
parent e517d72bee
commit f0ac477d2e
17 changed files with 88 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/Lean/Declaration.lean
View file

@ -78,23 +78,28 @@ def mkAxiomValEx (name : Name) (lparams : List Name) (type : Expr) (isUnsafe : B
@[export lean_axiom_val_is_unsafe] def AxiomVal.isUnsafeEx (v : AxiomVal) : Bool :=
v.isUnsafe
inductive DefinitionSafety where
| «unsafe» | safe | «partial»
deriving Inhabited, BEq, Repr
structure DefinitionVal extends ConstantVal where
value : Expr
hints : ReducibilityHints
isUnsafe : Bool
value : Expr
hints : ReducibilityHints
safety : DefinitionSafety
deriving Inhabited
@[export lean_mk_definition_val]
def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (isUnsafe : Bool) : DefinitionVal := {
def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := {
name := name,
lparams := lparams,
type := type,
value := val,
hints := hints,
isUnsafe := isUnsafe
safety := safety
}
@[export lean_definition_val_is_unsafe] def DefinitionVal.isUnsafeEx (v : DefinitionVal) : Bool :=
v.isUnsafe
@[export lean_definition_val_get_safety] def DefinitionVal.getSafetyEx (v : DefinitionVal) : DefinitionSafety :=
v.safety
structure TheoremVal extends ConstantVal where
value : Expr
@ -132,7 +137,7 @@ inductive Declaration where
| thmDecl (val : TheoremVal)
| opaqueDecl (val : OpaqueVal)
| quotDecl
| mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe`
| mutualDefnDecl (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
| inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
deriving Inhabited
@ -301,7 +306,7 @@ def toConstantVal : ConstantInfo → ConstantVal
| recInfo {toConstantVal := d, ..} => d
def isUnsafe : ConstantInfo → Bool
| defnInfo v => v.isUnsafe
| defnInfo v => v.safety == DefinitionSafety.unsafe
| axiomInfo v => v.isUnsafe
| thmInfo v => false
| opaqueInfo v => v.isUnsafe

3
src/Lean/Elab/Binders.lean
View file

@ -65,7 +65,8 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
let val ← elabTerm tactic type
let val ← instantiateMVars val
trace[Elab.autoParam]! val
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
addDecl decl
compileDecl decl
pure name

3
src/Lean/Elab/BuiltinNotation.lean
View file

@ -95,7 +95,8 @@ private def mkNativeReflAuxDecl (type val : Expr) : TermElabM Name := do
let decl := Declaration.defnDecl {
name := auxName, lparams := [], type := type, value := val,
hints := ReducibilityHints.abbrev,
isUnsafe := false }
safety := DefinitionSafety.safe
}
addDecl decl
compileDecl decl
pure auxName

4
src/Lean/Elab/Command.lean
View file

@ -582,7 +582,9 @@ unsafe def elabEvalUnsafe : CommandElab
let type ← inferType value
let decl := Declaration.defnDecl {
name := n, lparams := [], type := type,
value := value, hints := ReducibilityHints.opaque, isUnsafe := true }
value := value, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.unsafe
}
Term.ensureNoUnassignedMVars decl
addAndCompile decl
let elabMetaEval : CommandElabM Unit := runTermElabM (some n) fun _ => do

13
src/Lean/Elab/PreDefinition/Basic.lean
View file

@ -103,11 +103,12 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U
isUnsafe := preDef.modifiers.isUnsafe }
| DefKind.«abbrev» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.«abbrev», isUnsafe := preDef.modifiers.isUnsafe }
hints := ReducibilityHints.«abbrev»,
safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
| DefKind.«def» =>
Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1),
isUnsafe := preDef.modifiers.isUnsafe }
safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
addDecl decl
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
if compile && !preDef.kind.isTheorem then
@ -121,13 +122,13 @@ def addAndCompileNonRec (preDef : PreDefinition) : TermElabM Unit := do
def addNonRec (preDef : PreDefinition) : TermElabM Unit := do
addNonRecAux preDef false
def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do
def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit := do
let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => {
name := preDef.declName,
lparams := preDef.lparams,
type := preDef.type,
value := preDef.value,
isUnsafe := true,
safety := safety,
hints := ReducibilityHints.opaque
}
addDecl decl
@ -136,8 +137,8 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) : TermElabM Unit := do
applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
pure ()
def addAndCompileUnsafeRec (preDefs : Array PreDefinition) : TermElabM Unit := do
addAndCompileUnsafe $ preDefs.map fun preDef =>
def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := do
addAndCompileUnsafe (safety := DefinitionSafety.partial) <| preDefs.map fun preDef =>
{ preDef with
declName := Compiler.mkUnsafeRecName preDef.declName,
value := preDef.value.replace fun e => match e with

2
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -20,7 +20,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Uni
kind := DefKind.«opaque»,
value := inh
}
addAndCompileUnsafeRec preDefs
addAndCompilePartialRec preDefs
private def isNonRecursive (preDef : PreDefinition) : Bool :=
Option.isNone $ preDef.value.find? fun

2
src/Lean/Elab/PreDefinition/Structural.lean
View file

@ -433,7 +433,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
else do
let (preDefNonRec, state) ← run $ elimRecursion preDefs[0]
mapError (addNonRec preDefNonRec) (fun msg => m!"structural recursion failed, produced type incorrect term{indentD msg}")
addAndCompileUnsafeRec preDefs
addAndCompilePartialRec preDefs
addSmartUnfoldingDef preDefs[0] state
builtin_initialize

21
src/Lean/Elab/Print.lean
View file

@ -20,8 +20,12 @@ private def lparamsToMessageData (lparams : List Name) : MessageData :=
m := m ++ ", " ++ u
return m ++ "}"
private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := do
let m : MessageData := if isUnsafe then "unsafe " else ""
private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
let m : MessageData :=
match safety with
| DefinitionSafety.unsafe => "unsafe "
| DefinitionSafety.partial => "partial "
| DefinitionSafety.safe => ""
let m := if isProtected (← getEnv) id then m ++ "protected " else m
let (m, id) := match privateToUserName? id with
| some id => (m ++ "private ", id)
@ -29,20 +33,23 @@ private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : E
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
pure m
private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
let m ← mkHeader kind id lparams type isUnsafe
private def mkHeader' (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
mkHeader kind id lparams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
let m ← mkHeader kind id lparams type safety
let m := m ++ " :=" ++ Format.line ++ value
logInfo m
private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
logInfo (← mkHeader kind id lparams type isUnsafe)
logInfo (← mkHeader' kind id lparams type isUnsafe)
private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
printAxiomLike "Quotient primitive" id lparams type
private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
(ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
let mut m ← mkHeader "inductive" id lparams type isUnsafe
let mut m ← mkHeader' "inductive" id lparams type isUnsafe
m := m ++ Format.line ++ "constructors:"
for ctor in ctors do
let cinfo ← getConstInfo ctor
@ -52,7 +59,7 @@ private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindi
private def printIdCore (id : Name) : CommandElabM Unit := do
match (← getEnv).find? id with
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
| ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
| ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t

2
src/Lean/Elab/Term.lean
View file

@ -1361,7 +1361,7 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α :=
let decl := Declaration.defnDecl {
name := name, lparams := [], type := type,
value := value, hints := ReducibilityHints.opaque,
isUnsafe := true
safety := DefinitionSafety.unsafe
}
ensureNoUnassignedMVars decl
addAndCompile decl

3
src/Lean/KeyedDeclsAttribute.lean
View file

@ -102,7 +102,8 @@ def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment)
let name := `_regBuiltin ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do

2
src/Lean/Meta/Closure.lean
View file

@ -356,7 +356,7 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f
type := result.type,
value := result.value,
hints := ReducibilityHints.regular (getMaxHeight env result.value + 1),
isUnsafe := env.hasUnsafe result.type || env.hasUnsafe result.value
safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
}
trace[Meta.debug]! "{name} : {result.type} := {result.value}"
addDecl decl

3
src/Lean/Parser/Extension.lean
View file

@ -422,7 +422,8 @@ def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name)
let name := `_regBuiltinParser ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio]
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))

2
src/Lean/ParserCompiler.lean
View file

@ -83,7 +83,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
pure $ mkForall `_ BinderInfo.default paramTy ty
let decl := Declaration.defnDecl {
name := c', lparams := [],
type := ty, value := value, hints := ReducibilityHints.opaque, isUnsafe := false }
type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe }
let env ← getEnv
let env ← match env.addAndCompile {} decl with
| Except.ok env => pure env

34
src/kernel/declaration.cpp
View file

@ -62,15 +62,15 @@ axiom_val::axiom_val(name const & n, names const & lparams, expr const & type, b
bool axiom_val::is_unsafe() const { return lean_axiom_val_is_unsafe(to_obj_arg()); }
extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 is_unsafe);
extern "C" uint8 lean_definition_val_is_unsafe(object * v);
extern "C" object * lean_mk_definition_val(object * n, object * lparams, object * type, object * value, object * hints, uint8 safety);
extern "C" uint8 lean_definition_val_get_safety(object * v);
definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_unsafe):
definition_val::definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety):
object_ref(lean_mk_definition_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(),
hints.to_obj_arg(), is_unsafe)) {
hints.to_obj_arg(), static_cast<uint8>(safety))) {
}
bool definition_val::is_unsafe() const { return lean_definition_val_is_unsafe(to_obj_arg()); }
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)) {
@ -147,7 +147,7 @@ bool recursor_val::is_unsafe() const { return lean_recursor_is_unsafe(to_obj_arg
bool declaration::is_unsafe() const {
switch (kind()) {
case declaration_kind::Definition: return to_definition_val().is_unsafe();
case declaration_kind::Definition: return to_definition_val().get_safety() == definition_safety::unsafe;
case declaration_kind::Axiom: return to_axiom_val().is_unsafe();
case declaration_kind::Theorem: return false;
case declaration_kind::Opaque: return to_opaque_val().is_unsafe();
@ -191,19 +191,19 @@ static unsigned get_max_height(environment const & env, expr const & v) {
return h;
}
definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, bool unsafe) {
definition_val mk_definition_val(environment const & env, name const & n, names const & params, expr const & t, expr const & v, definition_safety s) {
unsigned h = get_max_height(env, v);
return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), unsafe);
return definition_val(n, params, t, v, reducibility_hints::mk_regular(h+1), s);
}
declaration mk_definition(name const & n, names const & params, expr const & t, expr const & v,
reducibility_hints const & h, bool unsafe) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, unsafe)));
reducibility_hints const & h, definition_safety safety) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), definition_val(n, params, t, v, h, safety)));
}
declaration mk_definition(environment const & env, name const & n, names const & params, expr const & t,
expr const & v, bool unsafe) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, unsafe)));
expr const & v, definition_safety safety) {
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
}
declaration mk_theorem(name const & n, names const & params, expr const & t, expr const & v) {
@ -218,17 +218,21 @@ declaration mk_axiom(name const & n, names const & params, expr const & t, bool
return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Axiom), axiom_val(n, params, t, unsafe)));
}
static definition_safety to_safety(bool unsafe) {
return unsafe ? definition_safety::unsafe : definition_safety::safe;
}
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params,
expr const & t, expr const & v, reducibility_hints const & hints) {
bool unsafe = use_unsafe(env, t) || use_unsafe(env, v);
return mk_definition(n, params, t, v, hints, unsafe);
return mk_definition(n, params, t, v, hints, to_safety(unsafe));
}
declaration mk_definition_inferring_unsafe(environment const & env, name const & n, names const & params,
expr const & t, expr const & v) {
bool unsafe = use_unsafe(env, t) && use_unsafe(env, v);
unsigned h = get_max_height(env, v);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), unsafe);
return mk_definition(n, params, t, v, reducibility_hints::mk_regular(h+1), to_safety(unsafe));
}
declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
@ -301,7 +305,7 @@ reducibility_hints const & constant_info::get_hints() const {
bool constant_info::is_unsafe() const {
switch (kind()) {
case constant_info_kind::Axiom: return to_axiom_val().is_unsafe();
case constant_info_kind::Definition: return to_definition_val().is_unsafe();
case constant_info_kind::Definition: return to_definition_val().get_safety() == definition_safety::unsafe;
case constant_info_kind::Theorem: return false;
case constant_info_kind::Opaque: return to_opaque_val().is_unsafe();
case constant_info_kind::Quot: return false;

13
src/kernel/declaration.h
View file

@ -92,13 +92,15 @@ public:
bool is_unsafe() const;
};
enum class definition_safety { unsafe, safe, partial };
/*
structure definition_val extends constant_val :=
(value : expr) (hints : reducibility_hints) (is_unsafe : bool)
*/
class definition_val : public object_ref {
public:
definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, bool is_unsafe);
definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety);
definition_val(definition_val const & other):object_ref(other) {}
definition_val(definition_val && other):object_ref(other) {}
definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
@ -109,7 +111,8 @@ public:
expr const & get_type() const { return to_constant_val().get_type(); }
expr const & get_value() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
reducibility_hints const & get_hints() const { return static_cast<reducibility_hints const &>(cnstr_get_ref(*this, 2)); }
bool is_unsafe() const;
definition_safety get_safety() const;
bool is_unsafe() const { return get_safety() == definition_safety::unsafe; }
};
typedef list_ref<definition_val> definition_vals;
@ -232,11 +235,11 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
definition_val mk_definition_val(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v, definition_safety safety);
declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
reducibility_hints const & hints, bool unsafe = false);
reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
bool unsafe = false);
definition_safety safety = definition_safety::safe);
declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v);
declaration mk_theorem(name const & n, names const & lparams, expr const & t, expr const & v);
declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);

12
src/kernel/environment.cpp
View file

@ -199,13 +199,18 @@ environment environment::add_opaque(declaration const & d, bool check) const {
environment environment::add_mutual(declaration const & d, bool check) const {
definition_vals const & vs = d.to_definition_vals();
if (empty(vs))
throw kernel_exception(*this, "invalid empty mutual definition");
definition_safety safety = head(vs).get_safety();
if (safety == definition_safety::safe)
throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as unsafe/partial");
bool safe_only = safety == definition_safety::partial;
/* Check declarations header */
if (check) {
bool safe_only = false;
type_checker checker(*this, safe_only);
for (definition_val const & v : vs) {
if (!v.is_unsafe())
throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as meta");
if (v.get_safety() != safety)
throw kernel_exception(*this, "invalid mutual definition, declarations must have the same safety annotation");
check_constant_val(*this, v.to_constant_val(), checker);
}
}
@ -216,7 +221,6 @@ environment environment::add_mutual(declaration const & d, bool check) const {
}
/* Check actual definitions */
if (check) {
bool safe_only = false;
type_checker checker(new_env, safe_only);
for (definition_val const & v : vs) {
check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());

4
src/library/compiler/util.cpp
View file

@ -545,7 +545,7 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
}
environment register_stage1_decl(environment const & env, name const & n, names const & ls, expr const & t, expr const & v) {
declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), true);
declaration aux_decl = mk_definition(mk_cstage1_name(n), ls, t, v, reducibility_hints::mk_opaque(), definition_safety::unsafe);
return env.add(aux_decl, false);
}
@ -555,7 +555,7 @@ bool is_stage2_decl(environment const & env, name const & n) {
environment register_stage2_decl(environment const & env, name const & n, expr const & t, expr const & v) {
declaration aux_decl = mk_definition(mk_cstage2_name(n), names(), t,
v, reducibility_hints::mk_opaque(), true);
v, reducibility_hints::mk_opaque(), definition_safety::unsafe);
return env.add(aux_decl, false);
}