Leonardo de Moura
|
38fc8a520d
|
chore: update stage0
|
2020-11-11 10:59:47 -08:00 |
|
Leonardo de Moura
|
fedd49de45
|
feat: remove if-then-else builtin parser
|
2020-11-11 10:57:06 -08:00 |
|
Leonardo de Moura
|
6970239ee3
|
chore: update stage0
|
2020-11-11 10:48:48 -08:00 |
|
Leonardo de Moura
|
d55f039a07
|
chore: do not use if-then-else notation at compileStxMatch
|
2020-11-11 10:47:02 -08:00 |
|
Leonardo de Moura
|
b882dff754
|
chore: do not use if-then-else notation at Prelude.lean
|
2020-11-11 10:37:19 -08:00 |
|
Leonardo de Moura
|
ab2ee0390d
|
chore: fix tests
|
2020-11-11 10:19:14 -08:00 |
|
Leonardo de Moura
|
5490235447
|
chore: remove renamed functions
|
2020-11-11 10:14:26 -08:00 |
|
Leonardo de Moura
|
86b0735e46
|
chore: update stage0
|
2020-11-11 10:10:17 -08:00 |
|
Leonardo de Moura
|
f17e226638
|
chore: naming convention
Example: `mkNameStr` => `Name.mkStr`
cc @Kha
|
2020-11-11 10:08:55 -08:00 |
|
Leonardo de Moura
|
df5b7fdc24
|
chore: naming convention
Use namespaces (e.g., `mkStxLit` ==> `Syntax.mkLit`)
cc @Kha
|
2020-11-11 09:55:23 -08:00 |
|
Leonardo de Moura
|
8ab9ca32b3
|
chore: update stage0
|
2020-11-11 08:29:38 -08:00 |
|
Leonardo de Moura
|
dbf99a17b6
|
chore: define notation using infix commands
|
2020-11-11 08:26:12 -08:00 |
|
Leonardo de Moura
|
231b7a0058
|
chore: update stage0
|
2020-11-11 07:35:34 -08:00 |
|
Leonardo de Moura
|
353aba579c
|
chore: remove builtin infix operators
|
2020-11-11 07:23:28 -08:00 |
|
Leonardo de Moura
|
383afb1114
|
chore: update stage0
|
2020-11-11 07:21:54 -08:00 |
|
Leonardo de Moura
|
7daeb7fffd
|
chore: fix test
|
2020-11-11 07:18:49 -08:00 |
|
Leonardo de Moura
|
f936fe306c
|
chore: fix annotation
|
2020-11-11 07:15:13 -08:00 |
|
Leonardo de Moura
|
bf7660ff5a
|
chore: avoid infix operators at Prelude.lean
We also fix the copyright date
|
2020-11-11 06:56:45 -08:00 |
|
Leonardo de Moura
|
4c80714b12
|
chore: do not use infix operators at Quotation.lean
Reason: macros need to be used before the notation is defined.
|
2020-11-11 06:56:45 -08:00 |
|
Leonardo de Moura
|
9c9d65e640
|
chore: move definitions needed by macros to Prelude.lean
|
2020-11-11 06:56:45 -08:00 |
|
Leonardo de Moura
|
ccf69ae69d
|
fix: missing file
|
2020-11-11 05:56:47 -08:00 |
|
Leonardo de Moura
|
22e6cc1c75
|
chore: update stage0
|
2020-11-10 18:48:58 -08:00 |
|
Leonardo de Moura
|
6ab0be952c
|
chore: merge src/Control files
Some of them were almost empty after the refactoring.
|
2020-11-10 18:47:23 -08:00 |
|
Leonardo de Moura
|
a8c791ecae
|
chore: remove dead files and functions
Remove obsolete combinators: `whenM`, `unlessM`, and `condM`
cc @Kha
|
2020-11-10 18:37:15 -08:00 |
|
Leonardo de Moura
|
30fb78d627
|
chore: update stage0
|
2020-11-10 18:11:10 -08:00 |
|
Leonardo de Moura
|
cca3bad0bb
|
feat: add Prelude.lean
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
|
2020-11-10 18:08:18 -08:00 |
|
Leonardo de Moura
|
3412c06059
|
chore: fix tests
|
2020-11-10 15:45:33 -08:00 |
|
Leonardo de Moura
|
687efdf974
|
chore: update stage0
|
2020-11-10 15:41:52 -08:00 |
|
Leonardo de Moura
|
c665d5e20a
|
chore: cleanup
|
2020-11-10 15:40:00 -08:00 |
|
Leonardo de Moura
|
7f364feeb5
|
chore: add Classical.lean, Equivalence, and cleanup
|
2020-11-10 14:55:34 -08:00 |
|
Leonardo de Moura
|
7e51020685
|
chore: move SizeOf to its own file
|
2020-11-10 14:43:03 -08:00 |
|
Leonardo de Moura
|
6c9c9c3955
|
chore: remove tactic framework dependency
|
2020-11-10 14:32:58 -08:00 |
|
Leonardo de Moura
|
7c393a1b3f
|
chore: cleanup
|
2020-11-10 14:06:11 -08:00 |
|
Leonardo de Moura
|
6ae2525e8f
|
chore: new prelude experiment
|
2020-11-10 14:02:58 -08:00 |
|
Leonardo de Moura
|
043fa5e16f
|
chore: update stage0
|
2020-11-10 12:35:22 -08:00 |
|
Leonardo de Moura
|
bd5c668347
|
feat: add helper functions for new Prelude.lean
|
2020-11-10 12:34:40 -08:00 |
|
Leonardo de Moura
|
de15bab918
|
chore: update stage0
|
2020-11-10 12:00:19 -08:00 |
|
Leonardo de Moura
|
1c01bd59be
|
chore: add numBitsEq
|
2020-11-10 11:59:16 -08:00 |
|
Leonardo de Moura
|
2daeb195b5
|
chore: use new names
|
2020-11-10 10:15:19 -08:00 |
|
Leonardo de Moura
|
cf0f4c04ed
|
chore: update stage0
|
2020-11-10 10:12:21 -08:00 |
|
Leonardo de Moura
|
2ef9199c56
|
chore: prepare to rename "predicate-like" classes
|
2020-11-10 10:12:21 -08:00 |
|
Sebastian Ullrich
|
e4f53fd92d
|
chore: adjust list & array spacing
|
2020-11-10 10:11:24 -08:00 |
|
Sebastian Ullrich
|
ce9be52ffb
|
feat: pretty print lists and arrays
|
2020-11-10 10:11:24 -08:00 |
|
Sebastian Ullrich
|
3665e3b7b5
|
feat: pretty print match
Fixes #177
|
2020-11-10 10:11:24 -08:00 |
|
Sebastian Ullrich
|
3d9f97574b
|
refactor: use and improve mkAppStx
|
2020-11-10 10:11:24 -08:00 |
|
Leonardo de Moura
|
33251fe069
|
chore: update stage0
|
2020-11-09 19:01:46 -08:00 |
|
Leonardo de Moura
|
7e8a7e6660
|
feat: elaborate fun/forall binder extensions
|
2020-11-09 19:00:40 -08:00 |
|
Leonardo de Moura
|
faa9ea3c98
|
chore: update stage0
|
2020-11-09 18:45:35 -08:00 |
|
Leonardo de Moura
|
25083fba9f
|
feat: extend binder syntax
|
2020-11-09 18:41:48 -08:00 |
|
Leonardo de Moura
|
defa45ae2f
|
feat: improve error message
when match-expression LHSs still contain metavariables after elaboration
|
2020-11-09 18:26:14 -08:00 |
|