|
Basic.lean
|
chore: remove clutter
|
2020-10-28 14:11:06 -07:00 |
|
Command.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Do.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Extension.lean
|
chore: cleanup
|
2020-10-29 10:24:16 -07:00 |
|
Extra.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Level.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Module.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
StrInterpolation.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Syntax.lean
|
feat: introduce suppressInsideQuot
|
2020-10-27 16:50:58 +01:00 |
|
Tactic.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Term.lean
|
feat: allow by ... at suffices
|
2020-10-27 13:05:13 -07:00 |
|
Transform.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
