Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Using type classes for logic programming
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
*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
You can’t perform that action at this time.