lang_closure |
Def (L![](FONT/up.png) )(l) == n: . (L n)(l)
Thm* Alph:Type, L:LangOver(Alph). (L![](FONT/up.png) ) LangOver(Alph)
|
lang_eq |
Def L = M == l:Alph*. L(l) ![](FONT/if_big.png) M(l)
Thm* Alph:Type{i}, L,M:LangOver(Alph). L = M Prop{i'}
|
lang_power |
Def (L n) == if n= 0 ![](FONT/delta_big.png) else ((L n-1) L) fi (recursive)
Thm* Alph:Type, L:LangOver(Alph), n: . (L n) LangOver(Alph)
|
languages |
Def LangOver(Alph) == Alph*![](FONT/dash.png) Prop
Thm* Alph:Type{i}. LangOver(Alph) Type{i'}
|
nat |
Def == {i: | 0 i }
Thm* Type
|
iff |
Def P ![](FONT/if_big.png) Q == (P ![](FONT/eq.png) Q) & (P ![](FONT/if_big.png) Q)
Thm* A,B:Prop. (A ![](FONT/if_big.png) B) Prop
|
lang_prod |
Def (L M)(l) == i:{0...||l||}. L(l[0..i ]) & M(l[i..||l|| ])
Thm* Alph:Type, M,N:LangOver(Alph). (M N) LangOver(Alph)
|
lang_sing |
Def ![](FONT/delta_big.png) (l) == null(l)
Thm* Alph:Type. ![](FONT/delta_big.png) LangOver(Alph)
|
eq_int |
Def i= j == if i=j true ; false fi
Thm* i,j: . i= j ![](FONT/bool.png)
|
int_iseg |
Def {i...j} == {k: | i k & k j }
Thm* i,j: . {i...j} Type
|
le |
Def A B == B < A
Thm* i,j: . i j Prop
|
rev_implies |
Def P ![](FONT/if_big.png) Q == Q ![](FONT/eq.png) P
Thm* A,B:Prop. (A ![](FONT/if_big.png) B) Prop
|
length |
Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
Thm* A:Type, l:A*. ||l||
Thm* ||nil|| ![](FONT/int.png)
|
segment |
Def as[m..n ] == firstn(n-m;nth_tl(m;as))
Thm* T:Type, as:T*, m,n: . (as[m..n ]) T*
|
null |
Def null(as) == Case of as; nil true ; a.as' false
Thm* T:Type, as:T*. null(as)
Thm* null(nil) ![](FONT/bool.png)
|
assert |
Def b == if b True else False fi
Thm* b: . b Prop
|
not |
Def A == A ![](FONT/eq.png) False
Thm* A:Prop. ( A) Prop
|
nth_tl |
Def nth_tl(n;as) == if n![](FONT/le.png) 0 as else nth_tl(n-1;tl(as)) fi (recursive)
Thm* A:Type, as:A*, i: . nth_tl(i;as) A*
|
firstn |
Def firstn(n;as)
== Case of as; nil nil ; a.as' if 0 < n a.firstn(n-1;as') else nil fi
(recursive)
Thm* A:Type, as:A*, n: . firstn(n;as) A*
|
tl |
Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A*. tl(l) A*
|
le_int |
Def i![](FONT/le.png) j == ![](FONT/not.png) j < i
Thm* i,j: . i![](FONT/le.png) j ![](FONT/bool.png)
|
lt_int |
Def i < j == if i < j true ; false fi
Thm* i,j: . i < j ![](FONT/bool.png)
|
bnot |
Def ![](FONT/not.png) b == if b false else true fi
Thm* b: . ![](FONT/not.png) b ![](FONT/bool.png)
|