Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/Addition.idr

Created August 2, 2013 00:04
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 david-christiansen/6136455 to your computer and use it in GitHub Desktop.
Save david-christiansen/6136455 to your computer and use it in GitHub Desktop.
Download ZIP
Using type classes for logic programming
Raw
Addition.idr
module Addition
class Plus (n : Nat) (m : Nat) (o : Nat) where {}
instance Plus Z m m where {}
instance Plus n m o => Plus (S n) m (S o) where {}
parameters (n : Nat, m : Nat)
using (o : Nat)
myplus : (Plus n m o) => Nat
myplus {o = o} = o
Raw
REPL
*Addition> myplus 2 4
6 : Nat
*Addition> myplus 90 2
92 : Nat
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment