
2 Apr
2013
2 Apr
'13
7:30 p.m.
On Tue, 2 Apr 2013, Daniel Peebles wrote:
It seems very similar to Ryan Ingram's post a few years back (pre-TypeNats): http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html The main difference is that he introduces the "knowledge" about zero vs. suc as a constraint, and you introduce it as a parameter. In fact, his induction function (which is probably what I'd call it too) is almost identical to your switch.
The answer to his post by Miguel Mitrofanov contains a caseNat that is exactly my 'switch'. I see I am four years late.