search

leanprover / leanprover.github.io

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

Misc #43

Closed dselsam closed 8 years ago

dselsam commented 8 years ago

Two commits are minor, and the third gets rid of sq and two sq lemmas at the cost of creating more instances during e-matching. See comment below.