pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update cases tactic to work on N type

Browse source
This commit is contained in:
Amanda Liu 2022-02-06 12:47:50 -05:00
parent f428750fdf
commit 1bff5420e2
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
FrapWithoutSets.v
View file

@ -229,6 +229,9 @@ Ltac cases E :=
((repeat match type of E with ((repeat match type of E with
| _ \/ _ => destruct E as [E | E] | _ \/ _ => destruct E as [E | E]
end) end)
|| (match type of E with
| N => destruct E using indN
end)
|| (is_var E; destruct E) || (is_var E; destruct E)
|| match type of E with || match type of E with
| {_} + {_} => destruct E | {_} + {_} => destruct E