Daniel Selsam
8b8814cfbe
fix(frontends/lean/inductive_cmd.cpp): fixes #1525
2017-05-01 14:57:25 -07:00
Sebastian Ullrich
0d02136a09
fix(frontends/lean/inductive_cmds): do not whnf pre-exprs
...
Fixes #1507
2017-04-25 17:47:29 -07:00
Gabriel Ebner
5f872912e0
refactor(shell/lean): set exit status 1 iff at least one error was reported
2017-03-23 08:57:56 +01:00
Leonardo de Moura
a897fd3f17
fix(frontends/lean): pattern matching in the declaration header
2017-03-16 01:09:12 -07:00
Daniel Selsam
7f56f23e70
chore(frontends/lean/inductive_cmds): allow sorrys
2017-03-15 14:06:56 -07:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08:00
Daniel Selsam
7dcc36277a
feat(frontends/lean/inductive_cmds.cpp): better resultant universe inference
2017-03-07 12:55:01 -08:00
Leonardo de Moura
32e6442d0a
feat(frontends/lean): no global universes in the frontend
2017-02-08 17:23:04 -08:00
Gabriel Ebner
7946b15511
feat(frontends/lean/elaborator): recover from most errors using sorry
2017-02-06 15:15:44 +01:00
Leonardo de Moura
3a4ef00f66
feat(frontends/lean): allow constructor parameters to be declared before ':'
2017-01-31 15:11:39 -08:00
Gabriel Ebner
5fdc737dfc
feat(library/tactic): store name of current declaration in tactic_state
2017-01-28 08:27:19 +01:00
Gabriel Ebner
a8df381d20
feat(*): parallel compilation
2016-11-29 11:12:40 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
Leonardo de Moura
338a46c225
fix(library/documentation): do not store doc strings for namespaces and declarations in the same name_map
2016-11-26 09:41:07 -08:00
Leonardo de Moura
97dd2f34d5
feat(library,frontends/lean): add basic doc string support
2016-11-25 18:52:56 -08:00
Sebastian Ullrich
bbb06dec70
fix(frontends/lean): pass around info_manager at more locations
2016-11-08 08:37:41 -08:00
Leonardo de Moura
6173d95d18
feat(library/module,frontends/lean): store line/column number information
2016-11-02 16:55:21 -07:00
Daniel Selsam
8d94dfd8e8
fix(inductive_cmd): intro rule names must be atomic identifiers
2016-10-13 10:12:08 -07:00
Daniel Selsam
3d2ff8a76d
chore(frontends/lean/inductive_cmd): readable name for ind result level placeholder
2016-10-05 15:10:21 -07:00
Leonardo de Moura
572751c56e
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
...
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
2016-09-29 17:56:35 -07:00
Leonardo de Moura
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
03e4fd1038
feat(frontends/lean,library): cleanup instance cmd, and use 'meta instance'
2016-09-24 12:33:25 -07:00
Leonardo de Moura
148da46481
feat(frontends/lean): 'mutual' and 'meta' are now keywords
2016-09-24 10:44:40 -07:00
Leonardo de Moura
165e2d5b97
chore(*): fix compilation warnings
2016-09-19 17:36:28 -07:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
e061e9acab
refactor(frontends/lean/elaborator): remove elaborator::ctx()
...
The plan is to make `type_context` a transient object in the elaborator.
2016-09-01 08:28:30 -07:00
Leonardo de Moura
a93eada058
feat(library/type_context): improved (and simplified) cache management for type_context
2016-08-23 17:56:58 -07:00
Leonardo de Moura
6aa11be6fd
fix(frontends/lean/inductive_cmds): memory leak
2016-08-23 15:36:46 -07:00
Daniel Selsam
a9b01991c2
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
...
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
2016-08-17 07:34:03 -07:00
Daniel Selsam
8aebea558a
feat(frontends/lean/inductive_cmds): scaffold for new inductive commands
2016-08-11 13:48:54 -07:00
