fix(library/type_context): preprocess_class: always solve universe mvars in inout
This commit is contained in:
parent
4fdf452b17
commit
0ca9eb16c1
2 changed files with 9 additions and 1 deletions
|
|
@ -3877,7 +3877,7 @@ For all these reasons, we have discarded this alternative design.
|
|||
expr type_context::preprocess_class(expr const & type,
|
||||
buffer<level_pair> & u_replacements,
|
||||
buffer<expr_pair> & e_replacements) {
|
||||
if (!has_expr_metavar(type))
|
||||
if (!has_metavar(type))
|
||||
return type;
|
||||
type_context::tmp_locals locals(*this);
|
||||
expr it = type;
|
||||
|
|
|
|||
8
tests/lean/run/inout_level.lean
Normal file
8
tests/lean/run/inout_level.lean
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
section bug
|
||||
variables (x y z : Type)
|
||||
variables (f : x → y) (g : y → z)
|
||||
variables (xy : set (x → y)) (yz : set (y → z)) (xz : set (x → z))
|
||||
--#check f ∈ xy
|
||||
--#check g ∈ yz
|
||||
#check (g ∘ f) ∈ xz --error
|
||||
end bug
|
||||
Loading…
Add table
Reference in a new issue