Leonardo de Moura
898a08a0c1
chore: avoid Has prefix in type classes
...
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
db9e390b4d
chore: remove new_frontend from tests
2020-10-25 09:16:38 -07:00
Leonardo de Moura
d6db541366
chore: cleanup
2020-09-28 19:05:48 -07:00
Leonardo de Moura
a0a724ddbd
fix: tests and elabDo
2020-09-26 19:12:01 -07:00
Leonardo de Moura
0511b73d80
feat: add replaceFVars
2020-09-22 14:24:03 -07:00
Leonardo de Moura
c996bc1f84
test: assertAfter
2020-09-17 19:35:16 -07:00
Leonardo de Moura
0d295560c3
feat: add replaceLocalDecl
...
It preserves the location of the local declaration.
@Kha This tactic is going to be used to fix another hygiene related bug in
Lean3 :)
Here is small repro for the problem.
```
example (m n k : ℕ) (h : 0 + n = m) (h : k = m) : ... :=
begin
-- Here `h : k = m` is accessible.
rw [nat.zero_add] at *
-- `h : k = m` is not accessible anymore, and it is a name for
-- the simplified `h : n = m` which was inaccessible before.
end
```
2020-09-17 19:27:48 -07:00
Leonardo de Moura
36bfe7b266
feat: add assertAfter tactic
2020-09-17 19:25:53 -07:00
Leonardo de Moura
b02cda0408
chore: move more tests to new frontend
2020-09-11 15:31:14 -07:00
Leonardo de Moura
102d2ae57d
fix: avoid unnecessary reduction
...
```lean
forallBoundedTelescope `(Nat -> IO Nat) 1 fun xs type => ...
```
should assign `IO Nat` to `type` instead of `IO.RealWorld -> ...`
2020-09-06 06:57:52 -07:00
Leonardo de Moura
555a3f0dcf
feat: new and improved mkAuxDefinition
2020-09-03 17:37:06 -07:00
Leonardo de Moura
f34fd3e6b4
refactor: move Closure.lean to Meta
...
We will need to improve the support for let-decls. We will use
the new `trackZeta`.
2020-09-03 11:54:08 -07:00
Leonardo de Moura
ad774ae397
feat: support for tracking which let-decls have been zeta expanded
2020-09-03 11:32:46 -07:00
