pretty-printing issues summary

[u5943321]

--add lines between tac results when printed:

--generate the letters: what after 26 alphabets?

--gravity: (f o g o h) does not have () around each pair, but (f o (g o h)) o i does, since it thinks the right i is trying to grab the h with it, but actually it is not.

[u5943321]

p2(F, E) o pa((i o p1(C, D)), (j o p2(C, D))) o
pa(f o p1(A, B), g o p2(A, B)) = p2(F, E) o
pa(i o f o p1(A, B), j o g o p2(A, B))

should not have () in pa((i o p1(C, D)), (j o p2(C, D))), should just be pa(i o p1(C, D), j o p2(C, D))

do not have the issue after edit pa into <>.

[u5943321]

add line between assumption formulas!

[u5943321]

pp the pa to be <>.

done, but maybe a TODO: add a dict of such special parens, and a predicate is_paren.

[u5943321]

pp: assumption list ugly indented like:

(f o p1(X, Y)) o pa(u, v) = (g o p2(X, Y)) o
---pa(u, v),
---f o u = g o
---v,
---f o p1(X, Y) o eqa(f o p1(X, Y), g o p2(X, Y)) = g o p2(X, Y) o
---eqa(f o p1(X, Y), g o p2(X, Y))

fixed, but by randomly trying adding blocks, do not really know why...

[u5943321]

|-
ismono(a) &
ismono(b) &
ALL (x : 1 -> A).
ALL (xb : 1 -> X).
a o xb = x ==> EXISTS (xb' : 1 -> Y). b o xb' = x ==>
EXISTS (h : X -> Y). b o h = a: thm

should heve () around the ant.

can only get:
ismono(a)
&
(ismono(b)
&
(! (x : 1 -> A).
! (xb : 1 -> X). (a o xb# = x# ==> (? (xb' : 1 -> Y). b o xb'# = x#))))
==>
(? (h : X -> Y). b o h# = a): form

not sure how to remove the () around the concl.

[u5943321]

tp((h o
pa(pa(p1(A, (N * exp(A, B))), p1(N, exp(A, B)) o
p2(A, (N * exp(A, B)))), ev(A, B) o
pa(p1(A, (N * exp(A, B))), p2(N, exp(A, B)) o
p2(A, (N * exp(A, B)))))))

should just be;

tp(h o
pa(pa(p1(A, (N * exp(A, B))), p1(N, exp(A, B)) o
p2(A, (N * exp(A, B)))), ev(A, B) o
pa(p1(A, (N * exp(A, B))), p2(N, exp(A, B)) o
p2(A, (N * exp(A, B))))))

after editting pa into <>, have:

readt "tp(h o pa(pa(p1(A, (N * exp(A, B))), p1(N, exp(A, B)) o p2(A, (N * exp(A, B)))), ev(A, B) o pa(p1(A, (N * exp(A, B))), p2(N, exp(A, B)) o p2(A, (N * exp(A, B))))))";
val it =
tp(h o <<p1(A, (N * exp(A, B))) , p1(N, exp(A, B)) o
p2(A, (N * exp(A, B)))> , ev(A, B) o
<p1(A, (N * exp(A, B))) , p2(N, exp(A, B)) o p2(A, (N * exp(A, B)))>>):
term

do not know if it is relevant, but no extra change.

[u5943321]

val f2 = rapf "(!b.P(a) & Q(c)) & Q(a)";
val f2 = (!b. (P(a) & Q(c))) & Q(a): form

should just be (!b. P(a) & Q(c)) & Q(a)

[u5943321]

rapf "eqa(f,g) o g = h"; seems loop, but it should just complain.

[u5943321]

A , B ,
(f : A -> B),
(t :
1 ->
eqo(coeqa((i1(B, B) o f), (i2(B, B) o f)) o i1(B, B),
coeqa((i1(B, B) o f), (i2(B, B) o f)) o i2(B, B)))
1.areiso(A, 0)
2.T

F
: gstk

click edit to see how it is ugly printted.

[u5943321]

areiso(eqo(coeqa((i1(B, B) o f), (i2(B, B) o f)) o i1(B, B),
coeqa((i1(B, B) o f), (i2(B, B) o f)) o i2(B, B)), 0)

should not have the ()