search

mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Finer eliminators for Enum #112

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Right now, the eliminator for Enum is switch, which takes a full bunch of 
branches. As discussed some time ago, we could have a finer notion of 
elimination over it: a real induction principle.

I suspect, it would look like this:

let inductionEnum (e : EnumU)(x : Enum e)(p : Sig ( e : EnumU ; Enum e ) -> Set)
              (mz : (e : EnumU) -> p [('cons 'x e) , 0])
          (ms : (e : EnumU)(x : Enum e) -> p [e , x] -> p [('cons 'x e) , 1 + x]) : p [e , x] ;

From this, we would implement switch and co.

This would be handy when doing induction on enumerations, with bits that turn 
up late.

Original issue reported on code.google.com by pedag...@gmail.com on 20 Sep 2010 at 11:52

GoogleCodeExporter commented 9 years ago 
I have implemented this eliminator, but not given its compile-time behaviour 
because I am not sure how we are supposed to do that now. We should be able to 
replace switch with a definition, but I've not done so yet.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100922104516-e29d1-aa0555e9be
f56c1dcb3f0ca3271f2a72cd593c67.gz

Original comment by adamgundry on 22 Sep 2010 at 10:56