Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
8958d1a5
Commit
8958d1a5
authored
Jan 22, 2016
by
Robbert Krebbers
Browse files
Improve simplifier for option to handle unions.
parent
2d9c59ac
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
4 additions
and
0 deletions
+4
0
prelude/option.v
prelude/option.v
+4
0
No files found.
prelude/option.v
View file @
8958d1a5
...
@@ 306,6 +306,10 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
...
@@ 306,6 +306,10 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=

_
=>
rewrite
decide_False
by
tac

_
=>
rewrite
decide_False
by
tac

_
=>
rewrite
option_guard_True
by
tac

_
=>
rewrite
option_guard_True
by
tac

_
=>
rewrite
option_guard_False
by
tac

_
=>
rewrite
option_guard_False
by
tac

H
:
context
[
None
∪
_
]

_
=>
rewrite
(
left_id_L
None
(
∪
))
in
H

H
:
context
[
_
∪
None
]

_
=>
rewrite
(
right_id_L
None
(
∪
))
in
H


context
[
None
∪
_
]
=>
rewrite
(
left_id_L
None
(
∪
))


context
[
_
∪
None
]
=>
rewrite
(
right_id_L
None
(
∪
))
end
.
end
.
Tactic
Notation
"simplify_option_equality"
"by"
tactic3
(
tac
)
:
=
Tactic
Notation
"simplify_option_equality"
"by"
tactic3
(
tac
)
:
=
repeat
match
goal
with
repeat
match
goal
with
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment