diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-18 18:16:20 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-01-18 18:16:20 -0500 |
| commit | b99dd6da3b6370bc225d3b501bda07c49fd29c12 (patch) | |
| tree | 6bf485279a6e792a9600dfc31fd0341e2d62a103 /src/Util | |
| parent | 70bdfbd3804d61535e280cecc042f73729664df4 (diff) | |
Define String.replace
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Strings/String.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/Strings/String.v b/src/Util/Strings/String.v index 3661d816f..adea76d48 100644 --- a/src/Util/Strings/String.v +++ b/src/Util/Strings/String.v @@ -283,4 +283,7 @@ Proof. { Abort. +Definition replace (from to s : string) : string + := concat to (split from s). + Notation NewLine := (String Ascii.NewLine ""). |