Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
David Swasey
coq-stdpp
Commits
1e946119
Commit
1e946119
authored
Sep 13, 2014
by
Robbert Krebbers
Browse files
Improve errors now that we use strings for names.
parent
70ee1472
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/stringmap.v
View file @
1e946119
...
...
@@ -7,6 +7,8 @@ and guarantees logarithmic-time operations. *)
Require
Export
fin_maps
.
Require
Import
Ascii
String
list
pmap
mapset
.
Infix
"+:+"
:
=
String
.
append
(
at
level
60
,
right
associativity
)
:
C_scope
.
Instance
assci_eq_dec
:
∀
a1
a2
,
Decision
(
a1
=
a2
)
:
=
ascii_dec
.
Instance
string_eq_dec
(
s1
s2
:
string
)
:
Decision
(
s1
=
s2
).
Proof
.
solve_decision
.
Defined
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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