[Agda] Numerical Programming in Agda

david rush kumoyuki at gmail.com
Mon Jul 1 13:36:30 CEST 2013

Hello all - 

I am working on a numerical programming project and it is increasingly looking 
like I am going to need something like Agda's fully dependent types in order 
to correctly express the structure of my code. The trouble is, it looks like 
almost no-one does any numerical programming in it, and I am loath to create 
my own prelude with the usual numeric type hierarchy (building up from Nat to 
Complex Floats). Well, I'd rather not if someone has already done it, anyway 

Google comes up with very few hits for "numerical programming in agda" and 
other similar searches. Can it really be that I am the first to try doing 
this? Does anyone have a pointer to pre-existing work which might help? 

david rush 

More information about the Agda mailing list