Commit af80361b authored by Robbert Krebbers's avatar Robbert Krebbers

Missing stuff in Proofmode.md.

Thanks to Janno for spotting this!
parent a24b19a9
Pipeline #3580 passed with stage
in 16 minutes and 31 seconds
...@@ -123,10 +123,10 @@ The later modality ...@@ -123,10 +123,10 @@ The later modality
hypotheses. If the argument `n` is not given, it strips one later if the hypotheses. If the argument `n` is not given, it strips one later if the
leftmost conjuct is of the shape `▷ P`, or `n` laters if the leftmost conjuct leftmost conjuct is of the shape `▷ P`, or `n` laters if the leftmost conjuct
is of the shape `▷^n P`. is of the shape `▷^n P`.
- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq level variables generating a hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq
`x1 ... xn`, the hypotheses given by the selection pattern `selpat`, and the level variables `x1 ... xn`, the hypotheses given by the selection pattern
spatial context. `selpat`, and the spatial context.
Induction Induction
--------- ---------
......
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