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

fix: error message produced by lean_mk_projections

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-22 17:40:18 -08:00
parent 800b4af15d
commit 8c2cb44ac0
2 changed files with 5 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Structure.lean
View file

@ -421,13 +421,13 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
pure { name := view.ctor.declName, type := type }
@[extern "lean_mk_projections"]
private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except String Environment
private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except KernelException Environment
private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : TermElabM Unit := do
let env ← getEnv
match mkProjections env structName projs isClass with
| Except.ok env => setEnv env
| Except.error msg => throwError msg
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
let env ← getEnv

8
src/library/constructions/projection.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <string>
#include <lean/sstream.h>
#include "kernel/kernel_exception.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "kernel/inductive.h"
@ -121,12 +122,7 @@ extern "C" object * lean_mk_projections(object * env, object * struct_name, obje
bool infer_mod = cnstr_get_uint8(p.raw(), sizeof(object*));
infer_kinds.push_back(infer_mod ? implicit_infer_kind::Implicit : implicit_infer_kind::RelaxedImplicit);
}
try {
new_env = mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0);
return mk_except_ok(new_env);
} catch (exception & ex) {
return mk_except_error(string_ref(ex.what()));
}
return catch_kernel_exceptions<environment>([&]() { return mk_projections(new_env, n, proj_names, infer_kinds, inst_implicit != 0); });
}
void initialize_def_projection() {