Leonardo de Moura
85e03da7db
feat(frontends/lean): add 'def' as shorthand for 'definition'
2016-09-23 08:25:16 -07:00
Leonardo de Moura
7ae778e925
feat(frontends/lean): generalize '~>' notation, and add alias '^.' for '~>'
2016-09-23 08:18:19 -07:00
Leonardo de Moura
d5b07336d9
chore(emacs): use \pr for projection notation
2016-09-22 07:29:02 -07:00
Leonardo de Moura
b55a17614a
feat(frontends/lean): structure instances
2016-09-21 22:52:43 -07:00
Leonardo de Moura
b7abd61579
feat(frontends/lean): change subtype notation (again)
...
We had conflicts with the set notation.
2016-09-21 17:02:18 -07:00
Leonardo de Moura
973bc5f1d6
feat(frontends/lean): add notation for 'sep'
2016-09-21 16:29:59 -07:00
Leonardo de Moura
c0ff9967af
feat(frontends/lean): add basic notation for collections
2016-09-21 16:20:57 -07:00
Leonardo de Moura
2b570e1eae
refactor(frontends/lean): remove old attributes
2016-09-21 14:22:17 -07:00
Leonardo de Moura
dde5f7ac70
feat(frontends/lean): add aliases such as: .1 for ~>1
2016-09-21 11:32:02 -07:00
Leonardo de Moura
b67216374c
feat(frontends/lean): projection notation
2016-09-21 11:14:41 -07:00
Leonardo de Moura
8657230435
chore(frontends/lean): new token for projections, and cleanup
2016-09-21 10:18:49 -07:00
Leonardo de Moura
5e5285ee67
refactor(library): rename pr1/pr2 ==> fst/snd
2016-09-21 09:48:39 -07:00
Leonardo de Moura
318ef761d3
feat(frontends/lean): lambda+anonymous_constructor+match notation
2016-09-21 08:49:05 -07:00
Leonardo de Moura
b2e1e920a9
chore(frontends/lean,library,linja): remove .ilean files
2016-09-20 08:43:45 -07:00
Leonardo de Moura
9df712581b
chore(frontends/lean): remove 'new_elaborator' option
2016-09-20 08:32:37 -07:00
Leonardo de Moura
465f898882
chore(library): remove lean2 old type checker
2016-09-19 22:21:19 -07:00
Leonardo de Moura
89f62edaf0
refactor(library): reduce dependecies on old code, simplify normalize module
2016-09-19 22:12:34 -07:00
Leonardo de Moura
668be38bb2
chore(library): remove old_type_context
2016-09-19 21:34:27 -07:00
Leonardo de Moura
a1d36b6c4d
chore(library): remove legacy_type_context
2016-09-19 21:31:21 -07:00
Leonardo de Moura
10b799c341
chore(library): remove more dead code
2016-09-19 21:26:33 -07:00
Leonardo de Moura
bbd10b99f7
chore(library): remove old type class resolution procedure
2016-09-19 21:22:02 -07:00
Leonardo de Moura
335242e9f1
chore(frontends/lean): remove info_annotation module
2016-09-19 21:19:31 -07:00
Leonardo de Moura
4c408d20d7
chore(bin): remove broken leantags
2016-09-19 19:57:30 -07:00
Leonardo de Moura
09687f70af
chore(frontends/lean/builtin_exprs): fix compilation warning
2016-09-19 19:50:30 -07:00
Leonardo de Moura
ba1df30099
chore(emacs): simplify emacs mode
...
The --server option has been deleted. In the future, we will replace it
with a simpler protocol (similar to the one we use for implementing
"show id/keyword information")
2016-09-19 19:41:22 -07:00
Leonardo de Moura
2a069a4d2a
chore(frontends/lean): remove server and info_manager
2016-09-19 18:44:03 -07:00
Leonardo de Moura
2969d8a8c6
chore(shell/CMakeLists): remove old tests
2016-09-19 18:44:03 -07:00
Leonardo de Moura
165e2d5b97
chore(*): fix compilation warnings
2016-09-19 17:36:28 -07:00
Leonardo de Moura
d2b400ac2c
chore(library): remove old unifier
2016-09-19 17:18:47 -07:00
Leonardo de Moura
c66dbf202b
chore(library/equations_compiler): remove old equation compiler
2016-09-19 17:13:30 -07:00
Leonardo de Moura
f6aba503ff
chore(frontends/lean): remove old elaborator
2016-09-19 17:10:28 -07:00
Leonardo de Moura
9f1a576e98
chore(frontends/lean): remove dead code from parser
2016-09-19 17:04:59 -07:00
Leonardo de Moura
5e4e1ba88a
chore(frontends/lean): delete old definition command
2016-09-19 16:50:25 -07:00
Gabriel Ebner
4dac796337
feat(library/local_context): make get_unused_name O(log(n))
2016-09-19 16:38:03 -07:00
Gabriel Ebner
3ef9149902
feat(library/tactic/tactic_state): add get_unused_name
2016-09-19 16:38:03 -07:00
Gabriel Ebner
8d06a88840
feat(library/tactic/intro_tactic): use get_unused_name
2016-09-19 16:38:03 -07:00
Leonardo de Moura
24f1cb2726
chore(frontends/lean): new_elaborator is now the default
2016-09-19 16:34:06 -07:00
Leonardo de Moura
c668185a1e
fix(frontends/lean/decl_util): bug add add_local_ref
2016-09-19 15:53:58 -07:00
Leonardo de Moura
f1a244b858
fix(frontends/lean/decl_util): bug at add_local_ref
2016-09-19 15:45:58 -07:00
Leonardo de Moura
ba5d608386
fix(frontends/lean/definition_cmds): create theorem when keyword 'theorem' is used
2016-09-19 14:48:16 -07:00
Leonardo de Moura
9a967001be
chore(library/equations_compiler/compiler): use exception until well_founded recursion support is implemented
2016-09-19 14:41:25 -07:00
Leonardo de Moura
a9578513ea
fix(library/type_context): use copy_tag when create auxiliary meta-variables
2016-09-19 13:59:08 -07:00
Leonardo de Moura
2153661642
fix(frontends/lean/parser): missing position information
2016-09-19 13:37:22 -07:00
Leonardo de Moura
e4553e0446
fix(library/type_context): bug in occurs check
2016-09-19 11:40:00 -07:00
Leonardo de Moura
0a6f571f07
fix(library/tactic/simplifier/simplifier): assertion
2016-09-19 11:29:03 -07:00
Leonardo de Moura
10f4a22fff
fix(frontends/lean/elaborator): try to synthesize pending type class instances before processing eliminator/recursor
2016-09-19 11:14:49 -07:00
Leonardo de Moura
677d3d4cf9
fix(frontends/lean/elaborator): ignore annotations around function when deciding which kind of elaborator strategy should be used
2016-09-18 19:10:13 -07:00
Leonardo de Moura
9d9f2b2636
fix(library/equations_compiler/structural_rec): bug at check_arg_type
2016-09-18 18:36:20 -07:00
Leonardo de Moura
4ba9644bd7
chore(library/rfl_lemmas): comment assertion
...
TODO: investigate why we have added it.
2016-09-18 18:20:18 -07:00
Leonardo de Moura
4e0e812811
fix(frontends/lean/builtin_exprs): patterns in do-notation
2016-09-18 18:19:51 -07:00
