Commit 2d1cd803 authored by Robbert Krebbers's avatar Robbert Krebbers

Document iInduction.

parent 9eb50174
Pipeline #2716 passed with stage
in 9 minutes and 19 seconds
......@@ -100,6 +100,13 @@ The later modality
- `iLöb (x1 ... xn) as "IH"` : perform Löb induction by generalizing over the
Coq level variables `x1 ... xn` and the entire spatial context.
Induction
---------
- `iInduction x as cpat "IH"` : perform induction on the Coq term `x`. The Coq
introduction pattern is used to name the introduced variables. The induction
hypotheses are inserted into the persistent context and given fresh names
prefixed `IH`.
Rewriting
---------
......
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