search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

Adopting a more disciplined approach to Sigma-splitting #49

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
Right now, we split Sigma-types like crazy, without distinction. It is just 
extraordinarily annoying.

I think we came up with the following simple firewall-like rule:

 * If it is in Prop, Sigma-split
 * After Elimination, Sigma-split the induction hypotheses
 * If it is a tuple of programming problems, Sigma-split
 * Otherwise, don't Sigma-split

A corollary is that there is no Sigma-splitting happening while working on a 
programming problem. It is up to the user to ask for it to happen.

Original issue reported on code.google.com by pedag...@gmail.com on 23 Aug 2010 at 1:37