Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A simple example showing how divide by zero can be restricted in Idris
module Main
%default total
myDivide : Nat -> (y:Nat) -> so (y /= 0) -> Nat
myDivide x y p = div x y
main : IO ()
main =
print (show (myDivide 3 1 oh)) -- compiles successfully
-- print (show (myDivide 3 0 oh)) -- throws an error at compile time
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.