michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add minor improvement to pretty printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-20 08:09:39 -07:00
parent d82c60a314
commit fbb021386c
2 changed files with 21 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
examples/ex10.lean Normal file
View file

@ -0,0 +1,19 @@
(* Define a "fake" type to simulate the natural numbers. This is just a test. *)
Variable Natural : Type
Variable lt : Natural -> Natural -> Bool
Variable zero : Natural
Variable one : Natural
Variable two : Natural
Variable three : Natural
Infix 50 < : lt
Axiom two_lt_three : two < three
Definition vector (A : Type) (n : Natural) : Type := Pi (i : Natural) (H : i < n), A
Definition const (A : Type) (n : Natural) (d : A) : vector A n := fun (i : Natural) (H : i < n), d
Definition update (A : Type) (n : Natural) (v : vector A n) (i : Natural) (d : A) : vector A n := fun (j : Natural) (H : j < n), if A (j = i) d (v j H)
Definition select (A : Type) (n : Natural) (v : vector A n) (i : Natural) (H : i < n) : A := v i H
Environment
Check select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
Eval select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
Check select

5
src/frontend/pp.cpp
View file

@ -478,7 +478,7 @@ class pp_fn {
condensed definitions. \see pp_abstraction_core.
*/
std::pair<expr, expr> collect_nested(expr const & e, expr T, expr_kind k, buffer<std::pair<name, expr>> & r) {
if (e.kind() == k) {
if (e.kind() == k && (!T || is_abstraction(T))) {
name n1 = get_unused_name(e);
r.push_back(mk_pair(n1, abst_domain(e)));
expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
@ -567,7 +567,6 @@ class pp_fn {
auto p = collect_nested(e, T, e.kind(), nested);
expr b = p.first;
T = p.second;
lean_assert(b.kind() != e.kind());
format head;
if (!T) {
head = is_lambda(e) ? g_lambda_fmt : g_Pi_fmt;
@ -845,7 +844,7 @@ class pp_formatter_cell : public formatter_cell {
it1 = abst_body(it1);
it2 = abst_body(it2);
}
if (!is_lambda(v) || is_pi(it1) || is_lambda(it2)) {
if (!is_lambda(v) || is_pi(it1)) {
return pp_definition(kwd, n, t, v);
} else {
lean_assert(is_lambda(v));