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
Iris
Iris
Commits
2ba9728f
Commit
2ba9728f
authored
Feb 27, 2016
by
Robbert Krebbers
Browse files
Improve notation for Case.
parent
603f0048
Pipeline
#182
passed with stage
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
heap_lang/notation.v
View file @
2ba9728f
...
...
@@ -25,7 +25,8 @@ 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' x1 => e1 | x2 => e2 'end'"
:
=
(
Case
e0
x1
e1
x2
e2
)
Notation
"'match:' e0 'with' 'injL' x1 => e1 | 'injR' 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"
).
Notation
"'()"
:
=
(
Lit
LitUnit
)
(
at
level
0
).
...
...
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