Leonardo de Moura
|
cd6acb5d1d
|
chore(library/pp_options): pp.binder_types true by default
|
2016-09-14 09:02:42 -07:00 |
|
Leonardo de Moura
|
4ae0ab79d9
|
feat(library/pp_options): show delayed_abstractions by default
|
2016-09-11 11:07:17 -07:00 |
|
Daniel Selsam
|
b0c5744eea
|
feat(inductive_compiler): support for mutually inductive types
|
2016-09-10 14:22:27 -07:00 |
|
Leonardo de Moura
|
a74f02546b
|
refactor(*): remove abbreviation command
|
2016-09-03 17:11:29 -07:00 |
|
Leonardo de Moura
|
20276f9b93
|
feat(frontends/lean/pp): pretty print character literals
|
2016-08-18 17:14:50 -07:00 |
|
Leonardo de Moura
|
52b66a1573
|
chore(frontends/lean/pp, library/pp_options): pp.lazy_abstraction ==> pp.delayed_abstraction
|
2016-08-03 18:45:47 -07:00 |
|
Leonardo de Moura
|
9fc222b9af
|
chore(library/pp_options): remove option pp.metavar_args
|
2016-07-31 16:00:21 -07:00 |
|
Leonardo de Moura
|
f18c84ca59
|
feat(frontends/lean/pp): add option for hiding coercions
|
2016-07-30 12:25:18 -07:00 |
|
Daniel Selsam
|
3ead9c1a59
|
doc(src/library/pp_options): improve description of pp.proofs option
|
2016-06-14 11:51:56 -07:00 |
|
Daniel Selsam
|
4d77f5ab2d
|
feat(src/frontends/lean/pp): option to print theorem statements instead of proof terms
Conflicts:
src/frontends/lean/pp.cpp
src/library/pp_options.cpp
|
2016-06-14 11:50:53 -07:00 |
|
Leonardo de Moura
|
546033633b
|
feat(frontends/lean/pp): add option for pretty printing lazy-abstractions
|
2016-06-14 09:24:51 -07:00 |
|
Leonardo de Moura
|
fe2b75aac7
|
fix(frontends/lean/pp,library/pp_options): 'pp.all true' should display binder types
|
2016-06-10 18:29:41 -07:00 |
|
Sebastian Ullrich
|
647078bd40
|
feat(frontends/lean/pp): add option to hide binder types
Replace old pp.hide_binder_types option
Conflicts:
src/frontends/lean/pp.cpp
src/library/pp_options.cpp
src/library/pp_options.h
|
2016-06-02 12:01:57 -07:00 |
|
Leonardo de Moura
|
6a9e5079c9
|
feat(library,frontends/lean/pp): add support for new string encoding
|
2016-05-24 16:20:43 -07:00 |
|
Leonardo de Moura
|
ca891c176e
|
feat(frontends/lean/pp): add option pp.hide_comp_irrelevant
It is true by default
|
2016-05-11 11:31:38 -07:00 |
|
Leonardo de Moura
|
da79cd7d95
|
feat(frontends/lean/pp): add option pp.hide_binder_types
|
2016-05-02 18:16:27 -07:00 |
|
Leonardo de Moura
|
774fa01b1a
|
chore(library/pp_options): reduce pp default limits
|
2016-02-04 14:55:21 -08:00 |
|
Leonardo de Moura
|
ba2cdc848a
|
feat(library/util, library/pp_options): add pp.goal.max_hypotheses
This commit also renames pp.compact_goals ==> pp.goal.compact
|
2015-12-30 12:43:03 -08:00 |
|
Leonardo de Moura
|
7f1800962a
|
feat(frontends/lean/pp): allow user to override pp.all setting
see #922
|
2015-12-11 10:40:48 -08:00 |
|
Sebastian Ullrich
|
6c34718cbc
|
chore(library,frontends/lean): remove option pp.extra_spaces
Obsoleted by improved pretty printer spacing
|
2015-10-13 09:52:35 -07:00 |
|
Leonardo de Moura
|
c76d92284f
|
feat(library/pp_options): add 'pp.all' option
|
2015-06-05 08:41:46 -07:00 |
|
Leonardo de Moura
|
8a89588079
|
refactor(library,library/tactic): move auxiliary procedures from tactic to library
|
2015-06-01 16:19:55 -07:00 |
|
Leonardo de Moura
|
937d6ac7b6
|
fix(frontends/lean/pp): print notation produces incorrect output
fixes #604
|
2015-05-19 09:57:13 -07:00 |
|
Leonardo de Moura
|
12bad8794b
|
feat(frontends/lean/pp): use 'assert' instead of 'have ... [visible]'
|
2015-05-08 10:02:15 -07:00 |
|
Leonardo de Moura
|
49bc56ec07
|
feat(frontends/lean/pp): improve pretty printer for prefix and postfix notation
closes #491
|
2015-03-25 16:45:58 -07:00 |
|
Leonardo de Moura
|
425aba9aa9
|
feat(library/pp_options): reduce default limits in the pretty printer
The goal is to avoid problems like the one described in issue #428
|
2015-02-25 14:04:17 -08:00 |
|
Leonardo de Moura
|
4364b7f926
|
feat(frontends/lean): pp.beta is true by default
Remark: there is one exception (command: print definition). For this
command pp.beta is still false.
|
2015-02-24 12:27:53 -08:00 |
|
Leonardo de Moura
|
43f849bf95
|
feat(frontends/lean/pp): add support for abbreviations in the pretty printer
closes #365
|
2015-02-10 18:27:02 -08:00 |
|
Leonardo de Moura
|
f344dd75c4
|
feat(library/pp_options): add get_pp_purify_locals_name
|
2015-01-08 11:55:08 -08:00 |
|
Leonardo de Moura
|
c33928f202
|
fix(library/pp_options): memory leak
|
2015-01-06 10:22:23 -08:00 |
|
Leonardo de Moura
|
69750c50c6
|
refactor(frontends/lean): move pp_options to library
|
2014-12-19 15:00:05 -08:00 |
|