blob: 803d957f089d193bc2575c4a62e60e8adf79037d (
plain)
1
2
3
4
5
6
7
8
9
10
|
resource StringOper = {
oper
SS : Type = {s : Str} ;
ss : Str -> SS = \x -> {s = x} ;
cc : SS -> SS -> SS = \x,y -> ss (x.s ++ y.s) ;
prefix : Str -> SS -> SS = \p,x -> ss (p ++ x.s) ;
}
|