Type requirement syntax

[pietervdvn]

In functions:

f  : a in Ord; b is Eq => a -> a -> b -> b -> Bool

In ADT defs:

data _ BalancedTree (a is Ord) = Top content:a left:(BalancedTree a) right:(BalancedTree a)
    | Nil

In class defs:

class Dict k v where:
    lookup : k -> Dict k v -> v

class Ord a => SortedSet a where:
    getMin : SortedSet a -> a

class SortedSet (a is Ord) where:
    getMin : SortedSet a -> a

class SortedSet a where a is Ord:
    getMin : SortedSet a -> a

[pietervdvn]

Finalized on the infix notation!

class SortedSet (a:Ord):

class SortedSet (a:Ord) in Collection a:

f : (a : Ord) -> a -> Bool

f : (a in Ord, Eq)

in, is, : are equivalent