Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
f1f28c42
Commit
f1f28c42
authored
Jan 12, 2016
by
Robbert Krebbers
Browse files
Tail recursive reverse operation on strings.
parent
466f1be9
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/strings.v
View file @
f1f28c42
...
...
@@ -16,6 +16,14 @@ Proof. solve_decision. Defined.
Instance:
Injective
(
=
)
(
=
)
(
String
.
append
s1
).
Proof
.
intros
s1
???
.
induction
s1
;
simplify_equality
'
;
f_equal
'
;
auto
.
Qed
.
(
*
Reverse
*
)
Fixpoint
string_rev_app
(
s1
s2
:
string
)
:
string
:=
match
s1
with
|
""
=>
s2
|
String
a
s1
=>
string_rev_app
s1
(
String
a
s2
)
end
.
Definition
string_rev
(
s
:
string
)
:
string
:=
string_rev_app
s
""
.
(
**
*
Encoding
and
decoding
*
)
(
**
In
order
to
reuse
or
existing
implementation
of
radix
-
2
search
trees
over
positive
binary
naturals
[
positive
],
we
define
an
injection
[
string_to_pos
]
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment