Leonardo de Moura
4450b8567d
fix: sigma notation precedence
2020-12-26 09:35:40 -08:00
Leonardo de Moura
7f9466a7ce
chore: use soft line breaks at if-then-else formatters
...
and remove `priority` leftover.
2020-12-24 08:35:43 -08:00
Leonardo de Moura
3655b1d9d0
chore: remove old if-then-else parsers
2020-12-24 08:25:14 -08:00
Leonardo de Moura
c9b42af537
chore: (prepare to) rename if-then-else parsers
...
We also add formatting directives to the new if-then-else parsers.
2020-12-24 08:20:07 -08:00
Leonardo de Moura
ccefe970dc
feat: store endPos at Log.lean
2020-12-23 19:09:41 -08:00
Wojciech Nawrocki
3fca58ea8c
feat: IO.FS.Handle.size
2020-12-23 20:00:36 +01:00
Sebastian Ullrich
3cdcdac921
feat: infer worker path
2020-12-23 20:00:36 +01:00
Marc Huisinga
088c3347cd
feat: adjust file worker for new IO features
2020-12-23 20:00:36 +01:00
Leonardo de Moura
839017fdae
feat: add macro tactical solve
2020-12-22 14:36:20 -08:00
Leonardo de Moura
9a1116d918
chore: remove <or>, first subsumes it
2020-12-22 14:10:08 -08:00
Leonardo de Moura
832c7412d6
feat: add first tactical
...
@Kha It has a few advantages over `<or>` (`<|>`).
- It is not an infix operator.
- It takes tactic sequences instead of tactics as arguments
For example, we can write
```
first
| apply h1; assumption
| exact y; exact h3; assumption
```
or
```
first apply h1; assumption | exact y; exact h3; assumption
```
instead of
```
(apply h1; assumption) <|> (exact y; exact h3; assumption)
```
2020-12-22 14:10:07 -08:00
Leonardo de Moura
56e2ff81b8
chore: ensure all term parsers have precedence >= min
2020-12-22 14:10:07 -08:00
Leonardo de Moura
69d83ecb86
chore: make sure term and tactic parsers have disjoint infix operators
2020-12-22 14:10:07 -08:00
Leonardo de Moura
7b813622c6
chore: increase precedence of |>, <|, $ parsers
...
@Kha Now, all parsers defined by `Init/Std/Lean` packages have
precedence >= `min` and <= `max`.
The only exception is `<|>` since it is an infix operator sharead with
the tactic DSL.
BTW, the meaning of `f $ a <|> b` changed with this commit.
It was `f (a <|> b)`, and now is `(f a) <|> b`. The problem is that
the precedence of the `$` parser is now greater than the `<|>` parser.
I will try another experiment where I make sure we do not "reuse"
term infix operators in the tactic DSL.
2020-12-22 14:10:07 -08:00
Leonardo de Moura
18aee9de30
fix: precedence issues at tactic DSL
2020-12-22 14:10:06 -08:00
Leonardo de Moura
f34bf82e0f
chore: move tactic parsers introMatch and match to Lean/Parser/Tactic
2020-12-22 07:11:06 -08:00
Leonardo de Moura
836fd46d90
feat: add OfNat instance for Fin
2020-12-21 16:38:53 -08:00
Leonardo de Moura
7723953188
chore: use instance (priority := <prio>)
2020-12-21 10:17:54 -08:00
Leonardo de Moura
c43e77d1a5
chore: fix Notation.lean
2020-12-21 09:47:11 -08:00
Sebastian Ullrich
cf73233dd2
refactor: use quotations & implicit token positions from getRef to clean up a bit
2020-12-21 17:32:36 +01:00
Sebastian Ullrich
cf7f60b470
feat: attach getRef position to symbols from quotations
...
/cc @leodemoura
2020-12-21 16:24:39 +01:00
Sebastian Ullrich
eeb0cad29e
feat: if let
...
/cc @leodemoura
2020-12-20 16:46:03 +01:00
Leonardo de Moura
339a4cf740
chore: remove defaultInstance for ToString
2020-12-19 19:10:42 -08:00
Leonardo de Moura
074259201e
feat: add helper classes for implementing parallel for
...
It is based on an approach suggested by Andrew Kent, and refined by
Sebastian Ullrich.
TODO: expand the the parallel `for`s at `Do.lean`.
2020-12-19 14:15:47 -08:00
Leonardo de Moura
bbcd2247f2
feat: extend valid set of valid auto bound names
...
@Kha The motivation was Andrew's example :)
Users often use `u₁`, `u1`, `u₂`, ... to name universe variables.
2020-12-19 12:36:19 -08:00
Leonardo de Moura
68701b86e4
feat: add Repr Name
2020-12-18 14:32:49 -08:00
Leonardo de Moura
793ffa2f11
feat: add helper class ReprAtom
2020-12-18 14:14:46 -08:00
Leonardo de Moura
b6905f66d6
fix: missing files
2020-12-18 11:47:00 -08:00
Leonardo de Moura
92f0afa424
chore: fix tests
2020-12-18 11:21:30 -08:00
Leonardo de Moura
5f6e66a53f
refactor: Repr
...
Modifications:
- Result type is `Format`
- It takes the context precedence like Haskell `Show`
2020-12-18 11:21:30 -08:00
Leonardo de Moura
2e11c3bdff
feat: dependencies
2020-12-18 11:21:30 -08:00
Leonardo de Moura
40bfafdadb
refactor: dependencies
2020-12-18 11:21:30 -08:00
Leonardo de Moura
15335efae2
refactor: move Format to Init package
...
We are going to use it to define `Repr` class.
2020-12-18 11:21:30 -08:00
Leonardo de Moura
67bcff3bc8
chore: use deriving DecidableEq
2020-12-17 17:48:23 -08:00
Leonardo de Moura
dee3c2c8d8
feat: improve deriving DecidableEq
2020-12-17 17:30:23 -08:00
Leonardo de Moura
87b6385bea
feat: add deriving DecidableEq
2020-12-17 17:30:23 -08:00
Leonardo de Moura
a4901f131b
feat: mark propDecidable as a scoped instance
2020-12-16 10:45:49 -08:00
Leonardo de Moura
7c865e7bd9
feat: sort instances by priority
2020-12-16 10:45:27 -08:00
Leonardo de Moura
fe08b28c7c
feat: add Array.insertionSort
2020-12-16 10:45:27 -08:00
Sebastian Ullrich
29c2023410
fix: adapt to new matchAlt syntax
2020-12-16 18:52:56 +01:00
Leonardo de Moura
7b67cd2c4a
chore: fix priorities
2020-12-16 07:11:02 -08:00
Leonardo de Moura
5b588b5984
fix: defaultInstance priorities
2020-12-16 06:52:55 -08:00
Leonardo de Moura
85e0b4fdb0
chore: add priority issue workaround
2020-12-15 21:25:37 -08:00
Leonardo de Moura
d4ae9e73b1
fix: missing comma
2020-12-15 20:29:28 -08:00
Leonardo de Moura
42a28261fd
chore: temporarily use 100000 as priority
2020-12-15 20:21:27 -08:00
Leonardo de Moura
d4f4eda0ea
feat: make sure expandMacro reduces prec and prio DSLs
2020-12-15 15:27:39 -08:00
Leonardo de Moura
abe7481453
feat: elaborate prio DSL
2020-12-14 16:25:10 -08:00
Leonardo de Moura
a2afd10060
feat: prio DSL
2020-12-14 16:07:02 -08:00
Leonardo de Moura
fcaf38d566
fix: handle prec DSL at infixl macro
2020-12-14 15:35:37 -08:00
Leonardo de Moura
911a433010
chore: remove temp comments
2020-12-14 15:10:41 -08:00
