multi_action |
Def multi_action(l; s; ASet)
== if null(l)![]() |
reverse |
Def rev(as) == Case of as; nil ![]() ![]()
Thm* |
tl |
Def tl(l) == Case of l; nil ![]() ![]()
Thm* |
aset_act |
Def a.act == 2of(a)
Thm* |
hd |
Def hd(l) == Case of l; nil ![]() ![]()
Thm* |
null |
Def null(as) == Case of as; nil ![]() ![]() ![]() ![]()
Thm*
Thm* null(nil) |
append |
Def as @ bs == Case of as; nil ![]() ![]()
Thm* |
pi2 |
Def 2of(t) == t.2
Thm* |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |