Forked from
Iris / Iris
Source project has a limited visibility.
Robbert Krebbers
authored
This fixes issue #57. I considered supporting these introduction patterns also in a nested fashion -- for example allowing `iDestruct foo as [H1 [{H1} H1 /= H2|H2]` -- but that turned out to be quite difficult. Where should we allow `/=`, `{H}` and `{$H}` exactly. Clearly something like `>/=` makes no sense, unless we adopt to some kind of 'stack like' semantics for introduction patterns as in ssreflect. Alternatively, we could only allow these patterns in the branches of the destructing introduction pattern `[... | ... | ...]` but that brings other complications, e.g.: - What to do with `(H1 & /= & H3)`? - How to distinguish the introduction patterns `[H _]` and `[_ H]` for destructing a spatial conjunction? We cannot simply match on the shape of the introduction pattern anymore, because one could also write `[_ H /=]`.
Name | Last commit | Last update |
---|---|---|
.. | ||
class_instances.v | ||
classes.v | ||
coq_tactics.v | ||
environments.v | ||
intro_patterns.v | ||
notation.v | ||
sel_patterns.v | ||
spec_patterns.v | ||
strings.v | ||
tactics.v |