leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

autocompletion bugs #12

Closed soonhokong closed 9 years ago

soonhokong commented 9 years ago

@leodemoura reported the followings:

soonhokong commented 9 years ago

The first item was fixed when I was at MSR. The second item is fixed by https://github.com/leanprover/leanprover.github.io/commit/219662bb6831b9385f21e7be85987dac5529b955 and https://github.com/leanprover/ace/commit/663876f674e497ba2f0a8b64346e3da60dadf49f.

eq.sy  => ctrl + space / choose 'eq.symm' => eq.symm
sub_lt => ctrl + space / choose 'int.sub_lt_right' => int_sub_lt_right