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
fd9be5e8ae
feat: add caseValues tactic
...
It is an auxiliary tactic for compiling pattern matching.
2020-08-06 15:37:00 -07:00
Leonardo de Moura
9084c4fafc
feat: add DepElim.lean
2020-08-05 16:03:33 -07:00
Leonardo de Moura
b959181132
feat: track unused alternatives
2020-08-05 15:53:25 -07:00
Leonardo de Moura
d1669049d6
feat: counterexamples
2020-08-05 15:34:03 -07:00
Leonardo de Moura
b642f3095f
chore: add another example reported in old issue
...
https://github.com/leanprover/lean/issues/1466
2020-08-05 13:18:13 -07:00
Leonardo de Moura
811cd31177
chore: add test for old issue
...
The new pattern matching compiler correctly compiles the patterns at
https://github.com/leanprover/lean/issues/1466
2020-08-05 13:00:13 -07:00
Leonardo de Moura
5aceea2632
feat: add "non variable" transition
2020-08-05 10:18:14 -07:00
Leonardo de Moura
b3dcd35661
fix: bugs at cases tactic
2020-08-05 09:44:26 -07:00
Leonardo de Moura
53c862e34b
chore: add another example using the generated eliminator
2020-08-04 19:15:56 -07:00
Leonardo de Moura
6be71b337f
refactor: add prototype2.lean
2020-08-04 18:35:11 -07:00
Leonardo de Moura
c778bea570
fix: isCompleteTransition
2020-08-04 13:25:27 -07:00
Leonardo de Moura
8c9ccb069a
fix: processVariable
2020-08-04 13:15:27 -07:00
Leonardo de Moura
dca2537524
refactor: use new FVarSubst
2020-08-04 13:12:25 -07:00
Leonardo de Moura
698d7e6dd1
fix: bug at processComplete
2020-08-03 17:58:38 -07:00
Leonardo de Moura
e43b5e27a1
feat: add processComplete
2020-08-03 17:02:53 -07:00
Leonardo de Moura
33d4732e58
fix: processVariable bug
2020-08-03 12:33:19 -07:00
Leonardo de Moura
9746f8ab25
feat: apply variable substitution to Alts
2020-08-03 10:12:10 -07:00
Leonardo de Moura
6bdb8f4726
feat: add processConstructor
2020-07-31 15:09:39 -07:00
Leonardo de Moura
3839e2a127
feat: processLeaf and processVariable
2020-07-30 17:18:05 -07:00
Leonardo de Moura
5a08e042df
chore: eliminator examples
2020-07-30 10:45:54 -07:00
Leonardo de Moura
0f598cca58
feat: create minor premises
2020-07-29 18:01:26 -07:00
Leonardo de Moura
53a7957b8e
chore: fix prototype
2020-07-29 18:01:26 -07:00
Leonardo de Moura
3dda98a40b
proto: checkpoint
2020-04-03 15:20:54 -07:00
Leonardo de Moura
73f5801d8a
proto: use generalizeTelescope
2020-03-30 11:47:03 -07:00
Leonardo de Moura
fdfa3fc0de
chore: minor
2020-03-19 17:01:59 -07:00
Leonardo de Moura
6ccade1738
proto: mkDepElim
2020-03-19 15:47:47 -07:00
Leonardo de Moura
2113e45dd0
chore: fix test
2020-03-19 09:29:07 -07:00
Leonardo de Moura
5b7d25727d
doc: matcher for values example
2020-03-13 06:39:13 -07:00
Leonardo de Moura
04f071606f
chore: cleanup example
2020-03-13 06:39:13 -07:00
Leonardo de Moura
a0090b378b
feat: move Array extensionality theorems to Init
2020-03-13 06:39:13 -07:00
Leonardo de Moura
a8c3322ac8
doc: expand dependent pattern matching support for array literals
2020-03-13 06:39:13 -07:00
Leonardo de Moura
65234064ec
doc: dep elim experiments
2020-03-11 19:25:38 -07:00
Leonardo de Moura
dc740307fa
doc: "plan" for matching array literals
...
The new equation compiler will generate code similar to
`matchArrayLit`. Of course, we will not use an auxiliary inductive datatype.
2020-03-11 12:00:11 -07:00
Leonardo de Moura
c05559a99d
refactor: cleanup
2019-12-06 14:41:39 -08:00
Leonardo de Moura
55626ba60d
chore(library/init/lean): disable new frontend for now
...
We are going to start making drastic changes in the parser,
elaborator, attributes, etc. Examples:
- No View objects. I am going to implement match_syntax.
- No RecT in the parser. I am going to implement parser extensions
using an approach similar to the one I used to implement environment
extensions.
- No Parsec. I will use an approach similar to the one used in the
experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser
It is easier to perform these changes with the new frontend disabled.
I will slowly re-active it as I apply the changes.
cc @kha
2019-06-05 15:26:43 -07:00
Leonardo de Moura
080c2dabde
chore(*): cleanup
2018-09-07 09:01:48 -07:00
Leonardo de Moura
54b45c19b3
chore(tmp/lean4.md): moved to google docs
2018-03-20 17:26:43 -07:00
Leonardo de Moura
c17e5b913b
doc(tmp/lean4): expand explicit reference counter section
2018-03-19 21:42:16 -07:00
Leonardo de Moura
f81f0452ee
doc(tmp/lean4): explicit reference counting
2018-03-19 19:18:02 -07:00
Leonardo de Moura
ae60d2bf48
doc(tmp/lean4): add SSA/SIL remark
2018-03-19 18:42:34 -07:00
Leonardo de Moura
78accd059c
doc(tmp/lean4): object memory layout
2018-03-19 18:33:35 -07:00
Leonardo de Moura
e7760eaa0b
doc(tmp/lean4): expr, level, name, ... in Lean
2018-03-19 17:39:46 -07:00
Leonardo de Moura
785466507a
doc(tmp/lean4): document the inline issue
2018-03-19 17:26:31 -07:00
Leonardo de Moura
d52b5a9f4f
doc(tmp/lean4): update notes
2018-03-19 17:21:11 -07:00
Leonardo de Moura
16f28315ee
doc(lean4): design notes
...
@kha I added some notes for the Lean4 branch. It is very unpolished.
2018-03-09 17:48:00 -08:00
Leonardo de Moura
8c9cee3efc
doc(tmp/fresh_name): document impact of new mk_fresh_name design on thread local caches
2018-02-01 18:06:19 -08:00
Leonardo de Moura
50a43da17c
doc(tmp/fresh_name): plan for fixing mk_fresh_name
...
@kha If you have time, could you please take a look and send feedback.
I may be forgetting other problems and issues related with `mk_fresh_name`.
2018-02-01 16:19:25 -08:00
