Ordered pairs in Idris

I implemented an ordered pair type in Idris. Took me a while.

https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr

Already has an inequality type. That may have been better to use.

Exploration and guesswork was necessary. How the heck do I get a hotkey for holes in atom?

The first couple Opairs are ordinary pairs. Just exploring the syntax.

I switched out of InEq which explicitly stores the number it is talking about to better match the equality type.

The Inequality type acts something like a mix of Nat and Equality.

My head hurts and I’m dehydrated.

 

 

Leave a Reply

Your email address will not be published. Required fields are marked *