IdrisProofs

ExampleProofs using Idris’s Elaborator and Pruviloj

This started as personal practice to learn about Idris' proof and Elaboration magic. However, since there is not much on the internet for these demonstrations I thought it would be best to make it public so people would have something to see and learn from.

Future examples will be added when they are added.

Anyone is invited to add and contribute.

What this is

Education for many of Idris' ideas and features

What this is not

Code Golf and Hacks. Some code may read very redundant, it probably is suppose to be that way.

Additional Notes about Code

• Most properties will be represented using Idris interfaces (in the same manner as mathematical classes), these are provided in the separate file properties.idr. This allows for easier organization and semantics.

Remember to compile with -p pruviloj