doc/tutorial-next/StringOper.gf


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) ;
}