Leonardo de Moura
|
4cfa4f0e9c
|
feat: add temporary hack
`mutual` + `partial` doesn't work yet.
|
2019-11-03 15:35:15 -08:00 |
|
Leonardo de Moura
|
b181ee5a4c
|
chore: typos
|
2019-11-02 14:45:17 -07:00 |
|
Leonardo de Moura
|
146aa71886
|
feat: reduce auxiliary recursors
|
2019-11-02 14:38:24 -07:00 |
|
Leonardo de Moura
|
f8c5face56
|
chore: update
|
2019-11-02 12:12:27 -07:00 |
|
Leonardo de Moura
|
ba7f2849dc
|
chore: use aux recursor extension implemented in Lean
|
2019-11-02 11:48:02 -07:00 |
|
Leonardo de Moura
|
1702579a76
|
chore: update stage0
|
2019-11-02 11:27:50 -07:00 |
|
Leonardo de Moura
|
359a78b902
|
feat: aux recursor extension in Lean
|
2019-11-02 11:24:52 -07:00 |
|
Leonardo de Moura
|
2d01621aba
|
feat: add TagDeclarationExtension helper
|
2019-11-02 10:59:06 -07:00 |
|
Leonardo de Moura
|
1a5de2c184
|
feat: add reduceProjectionFn
This is code for reducing user-facing projections functions created by
the `structure` command.
|
2019-11-02 10:26:38 -07:00 |
|
Leonardo de Moura
|
2d65b2ba9f
|
feat: reduce Expr.proj
|
2019-11-01 17:07:38 -07:00 |
|
Leonardo de Moura
|
638ceebab4
|
feat: helper functions
|
2019-11-01 17:07:26 -07:00 |
|
Leonardo de Moura
|
36f2bc987e
|
chore: TypeInference ==> TypeUtil
|
2019-11-01 16:24:49 -07:00 |
|
Leonardo de Moura
|
b3bce21e3b
|
feat: use CPS
|
2019-11-01 16:22:55 -07:00 |
|
Leonardo de Moura
|
1631fbde37
|
feat: add support for reducing recursor applications
|
2019-11-01 10:27:39 -07:00 |
|
Leonardo de Moura
|
823221840a
|
feat: add matchConst helper function
|
2019-11-01 10:20:34 -07:00 |
|
Leonardo de Moura
|
68bbba365c
|
feat: add isQuotRecStuck
|
2019-11-01 10:03:46 -07:00 |
|
Leonardo de Moura
|
cc6a72b789
|
feat: add reduceQuotRecAux
|
2019-11-01 09:55:29 -07:00 |
|
Leonardo de Moura
|
431a5de2b0
|
chore: add helper functions
|
2019-11-01 09:55:08 -07:00 |
|
Leonardo de Moura
|
32fdea86d9
|
feat: add isRecStuck
|
2019-11-01 09:31:19 -07:00 |
|
Leonardo de Moura
|
39d777435c
|
feat: add reduceRec
|
2019-11-01 08:40:56 -07:00 |
|
Daniel Selsam
|
5d4be4fd3c
|
doc: elabissue for simple namespace issue
|
2019-10-31 21:08:12 -07:00 |
|
Leonardo de Moura
|
ec71dd256f
|
chore: fix test
|
2019-10-31 21:01:31 -07:00 |
|
Leonardo de Moura
|
b78ab05360
|
feat: add reduceRecAux for reducing recursor applications
|
2019-10-31 20:58:59 -07:00 |
|
Leonardo de Moura
|
a4c2e72f1c
|
feat: helper functions
|
2019-10-31 20:58:30 -07:00 |
|
Leonardo de Moura
|
fd167c3829
|
chore: use Level instead of Univ
|
2019-10-31 20:13:44 -07:00 |
|
Leonardo de Moura
|
cae045bce8
|
chore: add helper function
|
2019-10-31 20:12:22 -07:00 |
|
Leonardo de Moura
|
8c7f514a9d
|
feat: expose instantiateLevelParams
|
2019-10-31 20:12:08 -07:00 |
|
Leonardo de Moura
|
51ce321c7e
|
feat: whnf skeleton
|
2019-10-31 17:40:05 -07:00 |
|
Leonardo de Moura
|
1b541219c9
|
chore: add helper function
|
2019-10-31 17:38:16 -07:00 |
|
Leonardo de Moura
|
665e8b3f4b
|
chore: style
|
2019-10-31 11:34:34 -07:00 |
|
Leonardo de Moura
|
952a707732
|
chore: cleanup
|
2019-10-31 11:00:05 -07:00 |
|
Leonardo de Moura
|
2df2f6cf62
|
feat: add processPostponed
|
2019-10-31 10:52:41 -07:00 |
|
Leonardo de Moura
|
1933d70aae
|
doc: explain why elaborator fails and propose alternative elaboration strategies
cc @dselsam @kha @rwbarton
|
2019-10-31 08:50:01 -07:00 |
|
Daniel Selsam
|
6cb4442349
|
doc: elabissue for overloads + list coercion
|
2019-10-31 08:04:00 -07:00 |
|
Leonardo de Moura
|
216e87e9a9
|
feat: add LBool
|
2019-10-30 19:30:08 -07:00 |
|
Leonardo de Moura
|
136b2c5171
|
fix: save updateLhs and updateRhs when postponing constraints
|
2019-10-30 19:29:21 -07:00 |
|
Leonardo de Moura
|
a7921e7013
|
feat: isDefEq for universe levels
|
2019-10-30 19:14:44 -07:00 |
|
Leonardo de Moura
|
e32402513d
|
feat: add hasAssignableLevelMVar
|
2019-10-30 18:23:30 -07:00 |
|
Leonardo de Moura
|
a9f3aa086d
|
feat: add Level.dec
|
2019-10-30 18:23:12 -07:00 |
|
Leonardo de Moura
|
f66b0d562c
|
chore: update stage0
|
2019-10-30 15:55:12 -07:00 |
|
Leonardo de Moura
|
ab88c312b5
|
chore: TypeContext => TypeInference
|
2019-10-30 15:51:37 -07:00 |
|
Leonardo de Moura
|
31767d025d
|
feat: improve AbstractMetavarContext interface
|
2019-10-30 15:02:33 -07:00 |
|
Leonardo de Moura
|
5f41cb69e4
|
feat: TmpMetavarContext
|
2019-10-30 14:56:01 -07:00 |
|
Leonardo de Moura
|
875d7657d9
|
feat: implement isEquiv in Lean
|
2019-10-30 14:55:40 -07:00 |
|
Leonardo de Moura
|
2f4a1f1239
|
test: universe level normalization function
|
2019-10-30 13:19:58 -07:00 |
|
Leonardo de Moura
|
4d5d3133bd
|
feat: universe level helper functions
|
2019-10-30 13:19:08 -07:00 |
|
Leonardo de Moura
|
00af75accf
|
chore: style
fix nonsense
|
2019-10-29 14:50:22 -07:00 |
|
Leonardo de Moura
|
4b7b95cd76
|
fix: missing file
LEAN_SMALL_ALLOCATOR is defined at `config.h`
|
2019-10-29 14:48:02 -07:00 |
|
Sebastian Ullrich
|
a1f352b4b1
|
fix: undefined pointer arithmetic in apply
|
2019-10-29 13:43:50 -07:00 |
|
Sebastian Ullrich
|
90b91760aa
|
fix: SMALL_ALLOCATOR=OFF
|
2019-10-29 13:41:16 -07:00 |
|