Leonardo de Moura
26a35e3ab1
feat: updateResultingUniverse
2020-07-15 16:32:22 -07:00
Leonardo de Moura
5ff8ad3b88
feat: add Level.replace and Expr.replaceLevel
2020-07-15 16:32:22 -07:00
Leonardo de Moura
94154113b5
feat: remove unused variables
2020-07-15 16:32:22 -07:00
Leonardo de Moura
fbf2d5d300
fix: do not print as arrow if binder_info is not the default one
2020-07-15 16:32:22 -07:00
Leonardo de Moura
4745519b54
feat: add Lean.Elab.CollectFVars
2020-07-15 16:32:22 -07:00
Sebastian Ullrich
b7f6f37079
chore: remove unreliable cache metrics
2020-07-15 17:16:04 +02:00
Leonardo de Moura
02de582941
feat: inductive datatype resulting universe inference
2020-07-14 17:18:58 -07:00
Leonardo de Moura
19b281e11e
fix: universe parameter generation
2020-07-14 17:15:15 -07:00
Leonardo de Moura
10fec63568
fix: missing resulting mctx
2020-07-14 16:50:08 -07:00
Leonardo de Moura
64bcb71b7a
chore: fix test
2020-07-14 16:44:02 -07:00
Leonardo de Moura
48c6c7c871
feat: report unused universe parameters
2020-07-14 16:40:56 -07:00
Leonardo de Moura
19595a0d03
fix: resolve pending universe metavars
2020-07-14 10:23:20 -07:00
Leonardo de Moura
455361d7d7
chore: update comment
2020-07-13 16:22:49 -07:00
Leonardo de Moura
d4ae4da222
feat: check given constructor resulting type
2020-07-13 16:22:49 -07:00
Leonardo de Moura
920343d36b
fix: unspecified constructor resulting type is not allowed inductive families
2020-07-13 16:22:49 -07:00
Leonardo de Moura
9960ca01f0
feat: reject protected constructors in a private inductive datatype
...
In a private inductive datatype, all constructors are private.
2020-07-13 16:22:49 -07:00
Leonardo de Moura
2744ae96bb
feat: check unsafe annotations in mutually inductive datatype declarations
2020-07-13 16:22:49 -07:00
Leonardo de Moura
2bf10b3d2c
feat: add inferMod field to CtorView
2020-07-13 16:22:49 -07:00
Leonardo de Moura
2cc2e71a53
feat: elaborate constructors
2020-07-13 16:22:49 -07:00
Leonardo de Moura
77ad630c80
test: inductive command
2020-07-13 16:22:49 -07:00
Leonardo de Moura
3fc6d8ce61
chore: improve constructor syntax
...
I think
```
inductive Foo
| private mk : Foo -> Foo
```
looks better than
```
inductive Foo
private | mk : Foo -> Foo
```
cc @Kha
2020-07-13 16:22:48 -07:00
Leonardo de Moura
d5f64f52a9
feat: add CtorView and modifier validation for inductive and constructors
2020-07-13 16:22:48 -07:00
Leonardo de Moura
6e12987dd9
feat: add declModifiers to constructor declarations
...
The goal is to allow users to attach doc strings and
`private/protected` to constructor declarations.
TODO: reject non applicable modifiers such as `unsafe` and `partial`.
cc @Kha
2020-07-13 16:22:48 -07:00
Leonardo de Moura
83431dc88e
feat: elaborate protected
2020-07-13 16:22:48 -07:00
Leonardo de Moura
fb6dfa4af2
chore: fix test
2020-07-13 16:22:48 -07:00
Leonardo de Moura
667f2ed601
feat: resolve inductive and ctor names
2020-07-13 16:22:48 -07:00
Leonardo de Moura
18fce4f455
feat: add Expr.inferImplicit
2020-07-13 16:22:48 -07:00
Sebastian Ullrich
162e63030c
leanmake: allow setting linker options
2020-07-13 21:39:04 +02:00
Leonardo de Moura
cda11dea25
feat: check universe parameters in mutually recursive inductive declaration
2020-07-11 08:01:36 -07:00
Leonardo de Moura
2949586244
feat: add local declarations for mutually inductive datatypes
2020-07-11 08:01:36 -07:00
Leonardo de Moura
c8636f2bf7
chore: generalize withDeclId
2020-07-11 08:01:36 -07:00
Leonardo de Moura
e26ec036ba
feat: add instantiateForall
2020-07-11 08:01:36 -07:00
Sebastian Ullrich
8826330862
chore: add slightly different config for new speedcenter
2020-07-10 17:28:58 +02:00
Sebastian Ullrich
96fb5ca4eb
chore: update temci
2020-07-10 17:28:58 +02:00
Sebastian Ullrich
fb02fbb867
fix: freeing Environments in tests
2020-07-10 07:42:26 -07:00
Sebastian Ullrich
719819bf49
fix: finally shouldn't call finalizer when finalizer throws
2020-07-10 07:42:26 -07:00
Sebastian Ullrich
c38f4fe837
feat: unsafe functions for freeing compacted regions
2020-07-10 07:42:26 -07:00
Sebastian Ullrich
ebd72d200f
fix: alloc/free mismatch detected by asan
2020-07-10 07:42:26 -07:00
Leonardo de Moura
f559576994
feat: inductive datatype header validation
2020-07-09 15:34:25 -07:00
Leonardo de Moura
c19c5e8427
chore: update stage0
2020-07-08 12:46:56 -07:00
Leonardo de Moura
a488ec903e
fix: remove old assertions
2020-07-08 12:45:53 -07:00
Leonardo de Moura
707ca63f87
chore: remove leftover MK_THREAD_LOCAL_GET
...
cc @Kha
2020-07-08 11:58:22 -07:00
Leonardo de Moura
d044e9f47e
chore: remove instance cache
...
If the missing cache generates perf problems in the future, we should
add the cache at `MetaM`.
cc @Kha
2020-07-08 09:40:34 -07:00
Sebastian Ullrich
00eda2f8c6
chore: update nixpkgs, changing back to LLVM 10
2020-07-08 12:14:49 +02:00
Sebastian Ullrich
b40ef65b39
feat: add IO.eprint(ln) for printing to stderr
...
Most useful when stdout is being consumed by another program
2020-07-06 09:22:47 -07:00
Sebastian Ullrich
0f6b9f5c94
chore: clean up stage 0 executable build
...
Previously we were building identical libInit/Std/Lean.a from the same stage0/stdlib sources. Now we simply link
everything right into libleancpp.a, again.
2020-07-03 19:26:00 +02:00
Leonardo de Moura
36c971546c
feat: add elabMutualInductive
2020-06-26 15:41:09 -07:00
Leonardo de Moura
e4b8a91e00
chore: update stage0
2020-06-26 12:49:42 -07:00
Leonardo de Moura
30f03ad18c
feat: add mutual syntax
2020-06-26 12:47:43 -07:00
Leonardo de Moura
1ad5b5984a
feat: add Inductive.lean
2020-06-26 12:44:13 -07:00
