Leonardo de Moura
deacb03802
feat: add isReadOnlyExprMVar
2019-11-28 05:34:12 -08:00
Leonardo de Moura
be9dab41ad
fix: abstractMVars
2019-11-27 10:53:25 -08:00
Leonardo de Moura
b1f9b7cd4d
feat: add AbstractMVars
2019-11-27 09:45:40 -08:00
Leonardo de Moura
005d03fc3d
feat: remove ignoreImplict workaround
2019-11-27 06:54:55 -08:00
Sebastian Ullrich
d5f30ddb83
fix: update-stage0
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
98b83e96cb
chore: do not build bin_lean_stage2 by default
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
682ad9f605
feat: stage 2 and 3 builds
...
While stage 1 is still the main build and the source of `bin/lean`, we now have optional targets
* lean_stage2, lean_stage3: build respective executable in `<build>/shell` from previous stage, compiling the stdlib
from scratch
* bin_lean_stage2: copy `lean_stage2` to `bin/` (stage 3 should always be identical to stage 2)
2019-11-27 05:53:22 -08:00
Sebastian Ullrich
2ad21d0f4c
feat: have --make take an optional .olean filename argument
...
Not documented since it is mostly useful for internal builds of further bootstrap stages
2019-11-27 05:53:22 -08:00
Leonardo de Moura
e99f8a9d22
chore: naming convention
...
suffix `?` should only be used for functions/methods returning `Bool`.
2019-11-27 05:50:31 -08:00
Leonardo de Moura
e8bd90a753
fix: performance issue introduced by 2809cea147
2019-11-27 05:43:28 -08:00
Leonardo de Moura
42fcf6e6e8
feat: add parameter ignoreImplicit
2019-11-26 17:56:07 -08:00
Leonardo de Moura
2809cea147
chore: remove DecidableEq workaround
...
We have better indexing now.
2019-11-26 17:30:18 -08:00
Leonardo de Moura
9a160a197a
fix: addGlobalInstance
2019-11-26 17:19:03 -08:00
Leonardo de Moura
81278c1509
feat: add instanceExtension
...
Use discrimination trees indexing type class instances.
2019-11-26 17:01:36 -08:00
Leonardo de Moura
55ab0f29e9
feat: break insert into two steps
...
Only the first step `Expr -> Array Key` requires the `MetaM` monad.
Motivation: we can save `(Array Key, Expr)` into .olean files, and
import modules without using `MetaM`.
2019-11-26 17:01:36 -08:00
Leonardo de Moura
f9376fe04b
feat: add withNewMCtxDepth
2019-11-26 17:01:36 -08:00
Leonardo de Moura
04417fafe8
chore: add missing instance
2019-11-26 17:01:36 -08:00
Leonardo de Moura
1f815ac521
feat: add forallMetaTelescope
2019-11-26 17:01:36 -08:00
Leonardo de Moura
4162eb1e08
fix: typo
2019-11-25 15:53:08 -08:00
Leonardo de Moura
856fb0c000
feat: use isProofQuick to implement isDefEqProofIrrel
2019-11-25 08:42:23 -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
ec0eed582e
chore: use isProof
2019-11-25 08:42:23 -08:00
Leonardo de Moura
120778585d
feat: add isProofQuick
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
882db55d11
feat: add reduce
2019-11-25 08:42:23 -08:00
Leonardo de Moura
0a7504a71a
feat: add isType and isProof
2019-11-25 08:42:23 -08:00
Leonardo de Moura
9a4facac29
feat: simplify Key.lt
2019-11-24 08:59:38 -08:00
Leonardo de Moura
6af26ede2b
fix: typo
2019-11-24 08:37:43 -08:00
Leonardo de Moura
0350c488d5
refactor: add Key.arity and simplify
2019-11-24 08:35:31 -08:00
Leonardo de Moura
e81f38c116
doc: add comment about representation
2019-11-24 08:17:44 -08:00
Leonardo de Moura
5842366416
feat: add DiscrTree.getUnify
2019-11-24 08:15:10 -08:00
Leonardo de Moura
c5afa18469
feat: add DiscrTree.getMatch
2019-11-24 07:56:57 -08:00
Leonardo de Moura
63a2466a03
fix: typo
2019-11-24 07:48:19 -08:00
Leonardo de Moura
2afb60cc07
fix: typo
2019-11-24 06:59:52 -08:00
Leonardo de Moura
8d30b7d3fb
doc: document DiscrTree module
2019-11-24 06:51:17 -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
4a6d0a8082
feat: projections of classes should not be reducible
2019-11-23 09:25:49 -08:00
Leonardo de Moura
84d582bf9a
feat: add DiscrTree.insert
2019-11-23 09:07:21 -08:00
Leonardo de Moura
c6048f0f94
feat: generalize binInsert
2019-11-23 08:20:20 -08:00
Leonardo de Moura
013bc5b589
feat: add modifyM
2019-11-23 07:37:33 -08:00
Leonardo de Moura
2e610227e4
feat: add Array.binInsert
2019-11-22 18:22:26 -08:00
Leonardo de Moura
69723b48c3
feat: add Array.insertAt
2019-11-22 17:42:27 -08:00
Leonardo de Moura
ea2d971bd3
chore: add isDefEq abbreviation for isExprDefEq
...
Most tactic users will never use `isLevelDefEq`.
2019-11-22 11:54:06 -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
b0ee140670
chore: trace messages
2019-11-22 11:18:48 -08:00
Leonardo de Moura
a9a27c77d8
feat: add helper combinators
2019-11-22 11:09:01 -08:00
Leonardo de Moura
ba7d14ebc2
fix: default path
2019-11-22 07:58:05 -08:00
Leonardo de Moura
b21559b338
chore: move Makefile.in
2019-11-22 07:48:04 -08:00
Leonardo de Moura
c445199747
chore: library/Init ==> src/Init
...
cc @Kha @dselsam @cipher1024
2019-11-22 06:06:05 -08:00
Leonardo de Moura
4adacf1413
chore: src/init ==> src/initialize
2019-11-22 04:59:13 -08:00
