Commit 2e9d27eb authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/iInduction_using' into 'master'

Document `iInduction ... using` tactic.

See merge request iris/iris!682
parents 0b082ac0 20145c5f
......@@ -240,6 +240,11 @@ Induction
+ `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
the selection pattern `selpat`, and the spatial context.
+ `iInduction x as cpat "IH" using t` : perform induction using the induction
scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
+ `iInduction x as cpat "IH" using t forall (x1 ... xn) "selpat"` : the above
variants combined.
Rewriting / simplification
Supports Markdown
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