Leonardo de Moura
|
1f815ac521
|
feat: add forallMetaTelescope
|
2019-11-26 17:01:36 -08:00 |
|
Leonardo de Moura
|
292603f8bb
|
chore: remove ParamInfo.proof field
It is an approximation because of dependent types.
Moreover, the new `isProofQuick` should make `isProof` much cheaper.
|
2019-11-25 08:42:23 -08:00 |
|
Leonardo de Moura
|
0592dae46f
|
chore: rename confusing field name ParamInfo.prop ==> ParamInfo.proof
The type of the parameter is a proposition, but the parameter itself
is a proof.
|
2019-11-25 08:42:23 -08:00 |
|
Leonardo de Moura
|
63d3429246
|
fix: reducibility setting should not hide non-definitions (constructors, inductive types, etc)
|
2019-11-23 09:36:22 -08:00 |
|
Leonardo de Moura
|
ad3f5b2490
|
feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext
|
2019-11-22 11:50:19 -08:00 |
|
Leonardo de Moura
|
a9a27c77d8
|
feat: add helper combinators
|
2019-11-22 11:09:01 -08:00 |
|
Leonardo de Moura
|
c445199747
|
chore: library/Init ==> src/Init
cc @Kha @dselsam @cipher1024
|
2019-11-22 06:06:05 -08:00 |
|