michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
5381 commits 3 branches 0 tags 28 MiB
Commit graph

85 commits

Author SHA1 Message Date
Leonardo de Moura
c845e44777 feat(frontends/lean): parse rewrite tactic 2015-02-04 11:51:39 -08:00
Leonardo de Moura
e2c41fca75 feat(frontends/lean): modify syntax for local notation 
The idea is to make it uniform with the syntax for defining local
attributes.
 2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed feat(frontends/lean): 'attribute' command is persistent by default 2015-01-26 11:51:17 -08:00
Leonardo de Moura
4f2e0c6d7f refactor(frontends/lean): add 'attribute' command 
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
 2015-01-24 20:23:21 -08:00
Leonardo de Moura
b172229a72 feat(frontends/lean): add 'match' expressions 
We reuse the equations infrastructure to compile them.
 2015-01-10 10:11:13 -08:00
Soonho Kong
f370871574 fix(emacs/lean-syntax): highlight axioms 
fix #382
 2014-12-30 14:25:19 -05:00
Leonardo de Moura
d2958044fd feat(frontends/lean): add multiple_instances command 
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
 2014-12-21 17:28:44 -08:00
Leonardo de Moura
6f78315aa4 refactor(*): add uniform names for "meta-objects" 2014-12-17 11:42:14 -08:00
Leonardo de Moura
d09bc95eaf feat(emacs): add Type0 highlight 2014-12-05 22:14:28 -08:00
Leonardo de Moura
e868ecce36 feat(frontends/lean): parse recursive equations 2014-12-04 17:03:21 -08:00
Leonardo de Moura
8dfd22e66c feat(frontends/lean): add 'prelude' command, and init directory 2014-11-30 17:03:08 -08:00
Leonardo de Moura
c08f4672e4 feat(library/tactic): add 'assert' tactic, closes #349 2014-11-29 21:34:49 -08:00
Leonardo de Moura
f51fa93292 feat(library/tactic): add 'fapply' tactic, closes #356 2014-11-29 19:20:41 -08:00
Leonardo de Moura
ad0dfb4c64 fix(emacs): syntax highlight for 'cases ... with ...' 2014-11-28 22:41:46 -08:00
Leonardo de Moura
c2602baf2b feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic 2014-11-28 19:33:11 -08:00
Leonardo de Moura
f8fa9f3344 feat(emacs): highlight 'inversion' tactic 2014-11-27 10:26:32 -08:00
Leonardo de Moura
63eafaae9a feat(emacs): add syntax-highlight for clear and revert tactics 2014-11-26 14:33:28 -08:00
Leonardo de Moura
f1e915a188 feat(frontends/lean): add 'find_decl' command 2014-11-23 23:00:59 -08:00
Leonardo de Moura
13fba433b0 feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327 2014-11-23 17:30:22 -08:00
Leonardo de Moura
47b6cfb28d feat(library/logic/if): add dependent if-then-else: dite 2014-11-22 09:56:32 -08:00
Leonardo de Moura
28c63e685b feat(frontends/lean): add '[local]' notation, closes #322 2014-11-16 21:15:04 -08:00
Leonardo de Moura
50973bb4f3 feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations 
To retrieve the previous behavior, we should use [strict] modifier
 2014-11-10 12:46:04 -08:00
Leonardo de Moura
bd5f3ec572 feat(emacs/lean-syntax): highlight [decls] modifier 2014-11-10 10:35:42 -08:00
Leonardo de Moura
c7992f2cac feat(frontends/lean): add [whnf] modifier to eval command 2014-11-08 10:19:29 -08:00
Soonho Kong
d861c78072 fix(emacs/lean-syntax): change comment symbols to be considered as punctuations 
Please read the documentation of "modify-syntax-entry":

"The first character of NEWENTRY should be one of the following:
  _           symbol constituent
  .           punctuation
"

Close: #306
 2014-11-07 17:48:21 -05:00
Leonardo de Moura
85d0521d48 feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305 2014-11-06 21:34:05 -08:00
Leonardo de Moura
ed83b7ff2a fix(emacs/lean-syntax): syntax highlight, issue #306 
1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
 2014-11-06 20:59:31 -08:00
Leonardo de Moura
4650791108 feat(frontends/lean): add 'print fields' command 2014-11-05 14:06:54 -08:00
Leonardo de Moura
defc2478b5 feat(frontends/lean): add 'record' as an alias for 'structure' command 2014-11-05 12:02:52 -08:00
Leonardo de Moura
101e9966fd fix(emacs/lean-syntax): bug in syntax highlight, examples do not have names 2014-11-03 18:32:18 -08:00
Leonardo de Moura
1e6f7cdbb4 chore(frontends/lean/decl_cmds): add 'example' command 
It is like a theorem, but it is discarded after checking
 2014-11-01 11:37:39 -07:00
Leonardo de Moura
591e566472 feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator 
This is part of #268
 2014-10-30 23:24:09 -07:00
Leonardo de Moura
9547e2d077 feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
Soonho Kong
17455d191b feat(emacs/lean-mode): add lean-info-mode for "*lean-info*" buffer 2014-10-29 14:33:05 -07:00
Soonho Kong
12824c3e27 fix(emacs/lean-syntax): fix Type1, Type2 highlight 2014-10-29 14:33:05 -07:00
Leonardo de Moura
e22eb3543c feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00
Leonardo de Moura
08e8161243 feat(emacs/lean-syntax): add 'eassumption' highlight 2014-10-26 15:45:26 -07:00
Leonardo de Moura
50948be66b fix(emacs/lean-syntax): syntax highlight for composite names in declarations 2014-10-26 09:27:17 -07:00
Leonardo de Moura
79d0347721 feat(library/tactic): add generalize tactic, closes #34 
Remark: the intros tactic has been added in a different commit: 7d0100a340
 2014-10-23 22:40:15 -07:00
Leonardo de Moura
c50227ea6e feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included 
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
 2014-10-22 18:11:09 -07:00
Leonardo de Moura
e95c7c5f70 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-22 17:29:50 -07:00
Leonardo de Moura
bb953b80aa feat(frontends/lean): reserve notation, closes #95 2014-10-21 15:39:47 -07:00
Leonardo de Moura
92acd9affc chore(emacs): do not highlight arbitrary types 2014-10-20 19:17:02 -07:00
Leonardo de Moura
7d0100a340 feat(library/tactic): add 'intros' tactic 2014-10-20 15:26:16 -07:00
Leonardo de Moura
e6606ef2ac feat(library/tactic): add 'rename' hypothesis tactic 2014-10-14 18:19:34 -07:00
Leonardo de Moura
ab90a350b3 fix(emacs/lean-syntax): syntax highlight for declarations with explicit universes 2014-10-13 06:52:36 -07:00
Leonardo de Moura
6a40f80612 fix(emacs/lean-syntax): glitch on syntax highlight 2014-10-11 10:56:28 -07:00
Leonardo de Moura
402a351937 feat(frontends/lean): add 'universes' command 2014-10-10 08:45:59 -07:00
Leonardo de Moura
d8572e249d feat(frontends/lean/builtin_cmds): add 'print classes' command 2014-10-07 17:30:57 -07:00
Leonardo de Moura
16562adb87 feat(frontends/lean): add 'coercions' and 'instances' to 'print' command, closes #71 2014-10-05 18:50:48 -07:00