pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #56 from al3623/cases_on_N

Browse source 
Update cases tactic to work on N type
This commit is contained in:
Adam Chlipala 2022-02-06 13:04:19 -05:00 committed by GitHub
commit c2260bb22b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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