max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc(src/library/pp_options): improve description of pp.proofs option

Browse source
This commit is contained in:
Daniel Selsam 2016-04-16 17:42:52 -07:00 • committed by Leonardo de Moura
parent 70c189d683
commit 3ead9c1a59
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/pp_options.cpp
View file

@ -160,7 +160,7 @@ void initialize_pp_options() {
register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT,
"(pretty printer) display implicit parameters");
register_bool_option(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS,
"(pretty printer) display proof terms");
"(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function");
register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS,
"(pretty printer) display coercionss");
register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,