That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all.
Ah, right! I must admit that it feels like an odd definition to me indeed. I see how "the first n natural numbers" is a finite set of n elements, but I don't see how the reverse is true. I mean, look here, a finite set of n elements: {1, 1, 1, 1}. 4 elements, and they're all valued 1. They're also not ordered. So your concept of taking an element from a finite set (in this case, let's say, 1, or maybe 1 instead) to uniquely identify an element in a vector sounds a bit odd to me :-)
Clearly, I'm the noob here, and maybe in this stage Idris just isn't meant for people not on Lambda the Ultimate, but if not, it's good that you intend do something about it :-)
Cause once again, I love the concept, and I'd love to program with this.
Comments
That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all.
Ah, right! I must admit that it feels like an odd definition to me indeed. I see how "the first n natural numbers" is a finite set of n elements, but I don't see how the reverse is true. I mean, look here, a finite set of n elements: {1, 1, 1, 1}. 4 elements, and they're all valued 1. They're also not ordered. So your concept of taking an element from a finite set (in this case, let's say, 1, or maybe 1 instead) to uniquely identify an element in a vector sounds a bit odd to me :-)
Clearly, I'm the noob here, and maybe in this stage Idris just isn't meant for people not on Lambda the Ultimate, but if not, it's good that you intend do something about it :-)
Cause once again, I love the concept, and I'd love to program with this.
The set {1, 1, 1, 1} has only one element, 1.
Oh fuck. Bags and sets.
I'm an idiot!
And that only 3 years out of university :-(