michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes)

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 17:55:59 -08:00
parent 9531203d9d
commit 186d910d0b
2 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/structure_cmd.cpp
View file

@ -22,6 +22,7 @@ Author: Leonardo de Moura
#include "library/unifier.h"
#include "library/module.h"
#include "library/aliases.h"
#include "library/coercion.h"
#include "library/explicit.h"
#include "library/protected.h"
#include "library/definitional/rec_on.h"
@ -641,6 +642,11 @@ struct structure_cmd_fn {
m_env = set_reducible(m_env, coercion_name, reducible_status::On);
save_def_info(coercion_name);
add_alias(coercion_name);
m_env = add_coercion(m_env, coercion_name, m_p.ios());
if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
// if both are classes, then we also mark coercion_name as an instance
m_env = add_instance(m_env, coercion_name);
}
}
}

17
tests/lean/run/record3.lean Normal file
View file

@ -0,0 +1,17 @@
import logic data.unit
structure point (A : Type) (B : Type) :=
mk :: (x : A) (y : B)
inductive color :=
red, green, blue
structure color_point (A : Type) (B : Type) extends point A B :=
mk :: (c : color)
constant foo (p: point num num) : num
constant p : color_point num num
set_option pp.coercions true
check foo p