lean4-htt

History

Leonardo de Moura 01003b79cc fix(library/init/meta/interactive): `simp [...] at ` closes #1675 After this commit, the following example works as expected. ``` example (p : nat → Prop) (a b : nat) : a = 0 ∧ b = 0 → p (a + b) → p 0 := begin intros h₁ h₂, simp [h₁] at , /- produces the state (p : nat → Prop) (a b : nat) h₁ : true h₂ : p 0 \|- p 0 -/ assumption end ``` as expected. Remark: the original issue raised by issue #1675 is actually solved by the `simp_all` tactic.	2017-07-01 20:50:46 -07:00
..
lean	fix(library/init/meta/interactive): `simp [...] at *`	2017-07-01 20:50:46 -07:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00

Leonardo de Moura 01003b79cc fix(library/init/meta/interactive): simp [...] at *

closes #1675

After this commit, the following example works as expected.
```
example (p : nat → Prop) (a b : nat) : a = 0 ∧ b = 0 → p (a + b) → p 0 :=
begin
  intros h₁ h₂,
  simp [h₁] at *,
  /- produces the state
     (p : nat → Prop) (a b : nat)
     h₁ : true
     h₂ : p 0
     |- p 0
  -/
  assumption
end
```
as expected.
Remark: the original issue raised by issue #1675 is actually solved by the
`simp_all` tactic.

2017-07-01 20:50:46 -07:00

lean fix(library/init/meta/interactive): simp [...] at * 2017-07-01 20:50:46 -07:00

.gitignore chore(tests/lean,shell/lean): run leantests and leanruntests in parallel 2017-03-30 06:04:00 +02:00