| module Main | |
| {- Divide x by y, as long as there is a proof that y is non-zero. The | |
| 'auto' keyword on the 'p' argument means that when safe_div is called, | |
| Idris will search for a proof. Either y will be statically known, in | |
| which case this is easy, otherwise there must be a proof in the context. | |
| 'so : Bool -> Type' is a predicate on booleans which only holds if the | |
| boolean is true. Essentially, we are making it a requirement in the type | |
| that a necessary dynamic type is done before we call the function -} |
On Understanding Data Abstraction, Revisited: http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf
CLU Reference Manual: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-225.pdf
Semantics Engineering with Redex: https://mitpress.mit.edu/books/semantics-engineering-plt-redex
On Understanding Types, Data Abstraction, and Polymorphism: http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf
Practical Foundations of Programming Languages: http://www.cs.cmu.edu/~rwh/plbook/book.pdf
