WAGS.Util

class Gate tf l r o | tf l r -> o

Instances

• Gate True l r l
• Gate False l r r

class TypeEqualTF (a :: Type) (b :: Type) (c :: Type) | a b -> c

Type-equality as a true/false assertion. Like TypeEquals, but allows us to encode the failure case.

Instances

• TypeEqualTF a a True
• TypeEqualTF a b False

class LtEq (a :: Nat) (b :: Nat) 

Assertion that a is less than b

Instances

• LtEq Z Z
• LtEq Z (Succ x)
• (LtEq x y) => LtEq (Succ x) (Succ y)