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
Pierre-Marie Pédrot
Iris
Commits
8076848a
Commit
8076848a
authored
Feb 27, 2016
by
Robbert Krebbers
Browse files
Notation for Case that is consistent with the constructor names.
parent
2ba9728f
Changes
1
Hide whitespace changes
Inline
Side-by-side
heap_lang/notation.v
View file @
8076848a
...
...
@@ -25,7 +25,7 @@ Coercion of_val : val >-> expr.
pretty printing. *)
Notation
"( e1 , e2 , .. , en )"
:
=
(
Pair
..
(
Pair
e1
e2
)
..
en
)
:
lang_scope
.
Notation
"' l"
:
=
(
Lit
l
%
Z
)
(
at
level
8
,
format
"' l"
).
Notation
"'match:' e0 'with' '
i
njL' x1 => e1 | '
i
njR' x2 => e2 'end'"
:
=
Notation
"'match:' e0 'with' '
I
njL' x1 => e1 | '
I
njR' x2 => e2 'end'"
:
=
(
Case
e0
x1
e1
x2
e2
)
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
lang_scope
.
Notation
"' l"
:
=
(
LitV
l
%
Z
)
(
at
level
8
,
format
"' l"
).
...
...
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