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

33 commits

Author SHA1 Message Date
Leonardo de Moura
4f0f739ea6 feat(library): remove occurrences of 'opaque' keyword 2015-05-08 16:40:03 -07:00
Leonardo de Moura
697d4359e3 refactor(library): add 'init' folder 2014-11-30 20:34:12 -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
1a7dd56f0f fix(library/tools/tactic): 'cases' argument precedence 2014-11-29 21:03:45 -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
2c0472252e feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00
Leonardo de Moura
e0debca771 feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses 2014-11-28 22:25:37 -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
ebd320a6b3 feat(library/tactic): add first step of 'inversion' tactic 2014-11-26 21:28:00 -08:00
Leonardo de Moura
f7deabfd19 feat(library/rename): add notation for rename 2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422 feat(library/tactic): add 'clears' and 'reverts' variants 2014-11-26 14:49:48 -08:00
Leonardo de Moura
2bd8f969d5 feat(library/tactic): add 'revert' tactic, closes #346 2014-11-26 14:23:42 -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
f16f215c2a refactor(data/num/string): break into pieces to reduce dependencies 2014-11-07 08:53:14 -08:00
Leonardo de Moura
e993486301 refactor(library/data/num): break into pieces to reduce dependencies 2014-11-07 08:24:29 -08:00
Leonardo de Moura
9547e2d077 feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -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
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
e750c9b67a feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode 2014-10-23 13:18:30 -07:00
Leonardo de Moura
00f9a10e82 refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic 
This change also enabled us to remove hacks used in the tests modified
by this commit.
 2014-10-23 10:26:19 -07:00
Leonardo de Moura
3aec70b92c feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time 2014-10-22 22:13:37 -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
9a316092d1 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic 2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92 feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics 2014-10-22 17:29:50 -07:00
Leonardo de Moura
e68007a727 fix(frontends/lean/builtin_tactics): adjust tactics precedence 2014-10-20 17:10:16 -07:00
Leonardo de Moura
58c9421bab refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70 2014-10-14 17:18:40 -07:00
Leonardo de Moura
e64d5c4a4a refactor(library/data/nat): use new operator '!' 2014-10-01 18:39:47 -07:00
Leonardo de Moura
97b1998def refactor(frontends/lean): replace '[opaque]' modifier with 'opaque 
definition', '[opaque]' is not a hint, but a kind of definition
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:26:36 -07:00
Leonardo de Moura
e51c4ad2e9 feat(frontends/lean): rename 'using' command to 'open' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 16:00:38 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:08:09 -07:00