From b99dd6da3b6370bc225d3b501bda07c49fd29c12 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 18 Jan 2019 18:16:20 -0500 Subject: Define String.replace --- src/Util/Strings/String.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Util') 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 ""). -- cgit v1.2.3