Skip to content

Instantly share code, notes, and snippets.

@gbluma

gbluma/divide_by_zero.idr

Created May 9, 2014 21:08
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gbluma/dd6dea90141fa21845ea to your computer and use it in GitHub Desktop.
Save gbluma/dd6dea90141fa21845ea to your computer and use it in GitHub Desktop.
Download ZIP
A simple example showing how divide by zero can be restricted in Idris
Raw
divide_by_zero.idr
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
@arpanetus
Copy link

No such variable so

Is that the expected behaviour? 🤔

@gbluma
Copy link
Author

gbluma commented Jul 16, 2021

I expect Idris has changed a bit in the last 7 years. I wouldn't consider bit of code to be accurate to the language any more.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment