forked from GitHub/gf-rgl
mapStr ; appPredefined in err monad
This commit is contained in:
@@ -22,7 +22,9 @@ resource Predef = {
|
|||||||
oper occur : Tok -> Tok -> PBool = variants {} ; -- test if occurs as substring
|
oper occur : Tok -> Tok -> PBool = variants {} ; -- test if occurs as substring
|
||||||
oper show : (P : Type) -> P -> Tok = variants {} ; -- convert param to string
|
oper show : (P : Type) -> P -> Tok = variants {} ; -- convert param to string
|
||||||
oper read : (P : Type) -> Tok -> P = variants {} ; -- convert string to param
|
oper read : (P : Type) -> Tok -> P = variants {} ; -- convert string to param
|
||||||
oper toStr : (P : Type) -> P -> Str = variants {} ; -- find the "first" string
|
oper toStr : (L : Type) -> L -> Str = variants {} ; -- find the "first" string
|
||||||
|
oper mapStr : (L : Type) -> (Str -> Str) -> L -> L = variants {} ;
|
||||||
|
-- map all strings in a data structure
|
||||||
|
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user