Leonardo de Moura
0ab46c2506
chore(library/type_context): simplify
2016-09-28 11:33:15 -07:00
Leonardo de Moura
fa252019f6
chore(library/print): clang++ compilation warning
2016-09-28 09:11:37 -07:00
Leonardo de Moura
e5ba0d7733
chore(*): cleanup
2016-09-27 17:30:57 -07:00
Leonardo de Moura
d59410cc41
refactor(kernel): support only proof irrelevant mode
2016-09-27 17:18:52 -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
9ef3ebbd5b
refactor(*): delete HoTT support
2016-09-27 16:33:39 -07:00
Leonardo de Moura
d4ed8baf3c
chore(util/thread): mark global as static
2016-09-27 15:53:49 -07:00
Leonardo de Moura
d7c3fce8a3
feat(library/init/coe,frontends/lean): more general coercions to fun
...
The new test dep_coe_to_fn.lean motivates the change.
2016-09-27 15:41:06 -07:00
Gabriel Ebner
d0ab6065c3
fix(frontends/lean): type check examples
2016-09-27 14:39:55 -07:00
Leonardo de Moura
c6ec659bf5
feat(frontends/lean): improve 'begin...end' blocks
2016-09-27 13:34:11 -07:00
Leonardo de Moura
6207dd0346
refactor(library/init): simplify has_emptyc type class
2016-09-27 10:03:57 -07:00
Leonardo de Moura
c6609543d0
chore(library/init): minor changes
2016-09-27 07:23:51 -07:00
Leonardo de Moura
6e6609f2aa
fix(frontends/lean): use coercions to sort at elaborate_type
2016-09-26 16:47:31 -07:00
Leonardo de Moura
8b110dec8d
fix(library/type_context): use scope_trace_env in trace msgs
2016-09-26 16:25:30 -07:00
Leonardo de Moura
dd8018eb04
fix(frontends/lean/elaborator): make coercion resolution more robust
2016-09-26 16:18:36 -07:00
Leonardo de Moura
b9b64b121c
feat(frontends/lean/elaborator): add show-goal support (Ctrl-c-g on Emacs)
2016-09-26 11:19:08 -07:00
Leonardo de Moura
78c6bc3a26
feat(frontends/lean): add step-by-step 'begin...end' block execution
2016-09-26 10:56:40 -07:00
Leonardo de Moura
ebe3b1047a
feat(library/vm/vm_exceptional): handle formatted_exception
2016-09-25 18:52:13 -07:00
Leonardo de Moura
3c71d7eda2
feat(frontends/lean,library/tactic/tactic_state): improve error localization
2016-09-25 18:40:41 -07:00
Leonardo de Moura
bbf21b4e65
feat(frontends/lean/begin_end_block): auto-quote identifiers
2016-09-25 17:25:21 -07:00
Leonardo de Moura
264b614f0d
fix(frontends/lean/elaborator): bug when checking for unassigned metavars
2016-09-25 17:22:45 -07:00
Leonardo de Moura
8b132c758a
feat(frontends/lean/begin_end_block): add basic auto-quotation
2016-09-25 17:03:12 -07:00
Leonardo de Moura
70ca497654
feat(frontends/lean/token_table): add ASCII notation for anonymous constructor
2016-09-25 13:48:52 -07:00
Leonardo de Moura
d5a28f91cc
refactor(library/init): reorganize files and cleanup notation
2016-09-25 13:37:45 -07:00
Leonardo de Moura
c11bcdc2fd
fix(library/type_context): incorrect context being used when tracing type classes resolution
2016-09-25 13:32:24 -07:00
Leonardo de Moura
6a49b2e18b
chore(library/vm,library/tactic): fix warnings produced by the new clang++
2016-09-25 11:14:28 -07:00
Leonardo de Moura
97261fcc48
feat(frontends/lean): add very basic 'begin ... end' block support
2016-09-24 21:27:27 -07:00
Leonardo de Moura
d944d78b1d
feat(frontends/lean/decl_cmds): attribute list must occur immediately after 'attribute' keyword
2016-09-24 18:40:57 -07:00
Leonardo de Moura
49cffc0b20
feat(frontends/lean): add compact notation for setting attributes suggested by Sebastian
2016-09-24 15:45:06 -07:00
Leonardo de Moura
d96f9327c5
fix(emacs): syntax highlight
2016-09-24 14:45:53 -07:00
Leonardo de Moura
5957022adb
feat(frontends/lean): add 'class' keyword
2016-09-24 14:32:01 -07:00
Leonardo de Moura
451cd177f0
feat(frontends/lean/pp): pretty print set_of notation
2016-09-24 13:55:02 -07:00
Leonardo de Moura
9ee553945c
feat(frontends/lean/brackets): set_of notation
2016-09-24 13:47:41 -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
6d9a9b46f3
chore(frontends/lean): cleanup
2016-09-23 16:26:21 -07:00
Leonardo de Moura
9991d61610
chore(library/init): cleanup
2016-09-23 14:53:17 -07:00
Leonardo de Moura
da27454c8c
chore(util): remove dead code
2016-09-23 14:29:13 -07:00
Leonardo de Moura
823357462e
feat(library/equations_compiler/structural_rec): validation
2016-09-23 13:50:55 -07:00
Leonardo de Moura
f00e6c0a96
feat(frontends/lean): anonymous instances
...
The instance name is synthesized automatically.
2016-09-23 13:34:34 -07:00
Leonardo de Moura
6bfd4eb9cf
feat(frontends/lean): add 'instance' keyword
2016-09-23 12:19:05 -07:00
Leonardo de Moura
177840bc36
fix(frontends/lean/elaborator): structure instance notation {...} for structures that have implicit fields
2016-09-23 11:32:12 -07:00
Leonardo de Moura
47b66b640f
fix(frontends/lean/structure_instance): incorrect assertions
2016-09-23 10:30:30 -07:00
Leonardo de Moura
96fe057d87
chore(frontends/lean/brackets): warnings
2016-09-23 10:19:33 -07:00
Leonardo de Moura
f9eaab8130
feat(frontends/lean/definition_cmds): improve error minimization
2016-09-23 10:16:46 -07:00
Leonardo de Moura
93106a6b02
chore(frontends/lean/builtin_exprs): error message consistency
2016-09-23 10:08:22 -07:00
Leonardo de Moura
9068dd9a88
chore(library/equations_compiler/equations): style
2016-09-23 10:05:18 -07:00
Leonardo de Moura
9a1ef1cc0d
fix(frontends/lean/elaborator): 'sorry' in quoted expressions
2016-09-23 09:34:00 -07:00
Leonardo de Moura
01f828a094
fix(library,frontends/lean): formatted_exception and elaborator_exception were missing main_expr when being cloned
2016-09-23 09:33:23 -07:00
Leonardo de Moura
c8e13cd391
feat(frontends/lean): minimize errors being reported
2016-09-23 09:20:31 -07:00
