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 |
|