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
Janno
iris-coq
Commits
d2147936
Commit
d2147936
authored
Jun 18, 2018
by
Ralf Jung
Browse files
backport heap_lang notation fix from gen_proofmode
parent
1d29427d
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lang.v
View file @
d2147936
...
...
@@ -531,11 +531,12 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
Export
heap_lang
.
(** Define some derived forms *)
Notation
Lam
x
e
:
=
(
Rec
BAnon
x
e
).
Notation
Let
x
e1
e2
:
=
(
App
(
Lam
x
e2
)
e1
).
Notation
Seq
e1
e2
:
=
(
Let
BAnon
e1
e2
).
Notation
LamV
x
e
:
=
(
RecV
BAnon
x
e
).
Notation
LetCtx
x
e2
:
=
(
AppRCtx
(
LamV
x
e2
)).
Notation
SeqCtx
e2
:
=
(
LetCtx
BAnon
e2
).
Notation
Lam
x
e
:
=
(
Rec
BAnon
x
e
)
(
only
parsing
).
Notation
Let
x
e1
e2
:
=
(
App
(
Lam
x
e2
)
e1
)
(
only
parsing
).
Notation
Seq
e1
e2
:
=
(
Let
BAnon
e1
e2
)
(
only
parsing
).
Notation
LamV
x
e
:
=
(
RecV
BAnon
x
e
)
(
only
parsing
).
Notation
LetCtx
x
e2
:
=
(
AppRCtx
(
LamV
x
e2
))
(
only
parsing
).
Notation
SeqCtx
e2
:
=
(
LetCtx
BAnon
e2
)
(
only
parsing
).
Notation
Match
e0
x1
e1
x2
e2
:
=
(
Case
e0
(
Lam
x1
e1
)
(
Lam
x2
e2
))
(
only
parsing
).
Notation
Skip
:
=
(
Seq
(
Lit
LitUnit
)
(
Lit
LitUnit
)).
Notation
Match
e0
x1
e1
x2
e2
:
=
(
Case
e0
(
Lam
x1
e1
)
(
Lam
x2
e2
)).
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