Skip to content
Snippets Groups Projects
Commit 72bf1989 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'inh-string' into 'master' 

Strings are inhabited

See merge request !70
parents 53e311e5 a5a851f5
No related branches found
No related tags found
1 merge request!70Strings are inhabited
Pipeline #16773 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
theories/strings.v
+ 2
− 0
View file @ 72bf1989
......@@ -23,6 +23,8 @@ Proof. solve_decision. Defined.
Instance string_app_inj : Inj (=) (=) (String.append s1).
Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
Instance string_inhabited : Inhabited string := populate "".
(* Reverse *)
Fixpoint string_rev_app (s1 s2 : string) : string :=
match s1 with
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment