Commit cceb5c12 authored by Ralf Jung's avatar Ralf Jung

expand HeapLang docs a bit

parent 336a8c7d
...@@ -46,6 +46,11 @@ Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`) ...@@ -46,6 +46,11 @@ Noteworthy is the fact that functions (`rec:`, `λ:`) in the value scope (`%V`)
are *locked*. This is to prevent them from being unfolded and reduced too are *locked*. This is to prevent them from being unfolded and reduced too
eagerly. eagerly.
The widely used `#` is a short-hand to turn a basic literal (an integer, a
location, a boolean literal or a unit value) into a value. Since values coerce
to expressions, `#` is widely used whenever a Coq value needs to be placed into
a HeapLang term.
## Tactics ## Tactics
HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment