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

chore: remove unnecessary approximation that just complicates the code

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-14 10:57:34 -08:00
parent 6b94d3fba9
commit f31fcbba24
2 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/Init/Lean/Meta/ExprDefEq.lean
View file

@ -322,7 +322,9 @@ do lctx ← getLCtx;
and all examples we have identified are in Init/Control.
A3) `a₁ ... aₙ` are not pairwise distinct (failed condition 1).
We can approximate again, but the limitations are very similar to the previous one.
In Lean3, we would try to approximate this case using an approach similar to A2.
However, this approximation complicates the code, and is never used in the
Lean3 stdlib and mathlib.
A4) `t` contains a metavariable `?m'@C'` where `C'` is not a subprefix of `C`.
(approximated) solution: restrict the context of `?m'`

6
src/library/type_context.cpp
View file

@ -1869,11 +1869,7 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
} else {
if (std::any_of(locals.begin(), locals.end(),
[&](expr const & local) { return local_name(local) == local_name(arg); })) {
/* m is of the form (?M ... l ... l ...) where l is a local constant. */
if (quasi_pattern_unif_approx()) {
/* workaround A3 */
add_locals = false;
} else if (fo_unif_approx()) {
if (fo_unif_approx()) {
use_fo = true;
add_locals = false;
} else {