@@ -5,6 +5,8 @@
5||| other metric of size.
5||| other metric of size.
6module Prelude.WellFounded
6module Prelude.WellFounded
8import Prelude.Nat
10import Prelude.Nat
9import Prelude.List
11import Prelude.List
10import Prelude.Uninhabited
12import Prelude.Uninhabited
@@ -128,3 +130,6 @@ implementation Sized Nat where
129implementation Sized (List a) where
131implementation Sized (List a) where
130 size = length
132 size = length
134+implementation (Sized a, Sized b) => Sized (Pair a b) where
135+ size (x,y) = Nat.plus (size x) (size y)