Commit 8dfda06c authored by Ralf Jung's avatar Ralf Jung
Browse files

mention how to use iLöb for recursive functions

parent 0cdad2cb
Pipeline #18543 passed with stage
in 14 minutes and 1 second
......@@ -105,6 +105,12 @@ Further tactics:
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
To verify a recursive function, use `iLöb`. Make sure you do `wp_pures` before
running `iLöb`; otherwise the induction hypothesis will likely not be applicable
when you need it. (This makes sure that all administrative redexes are reduced
in your induction hypothesis, just like we state our `WP` specifications with
all of the redexes reduced.)
## Notation and lemmas for derived notions involving a thunk
Sometimes, it is useful to define a derived notion in HeapLang that involves
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