Add implementation of Sized for Pair type
commit62695fc8dfc84a7397eccffd2efa9070166f0c97
authorZack Grannan <zgrannan@gmail.com>
dateMon 30 Jul 2018, 08:56 (8 years ago)
parent86126a7
libs/prelude/Prelude/WellFounded.idr+5
@@ -5,6 +5,8 @@
55||| other metric of size.
66module Prelude.WellFounded
77
8+import Builtins
9+
810import Prelude.Nat
911import Prelude.List
1012import Prelude.Uninhabited
@@ -128,3 +130,6 @@ implementation Sized Nat where
128130
129131implementation Sized (List a) where
130132 size = length
133+
134+implementation (Sized a, Sized b) => Sized (Pair a b) where
135+ size (x,y) = Nat.plus (size x) (size y)