Merge pull request #4528 from zgrannan/add-sized-pair
Add implementation of Sized for Pair type
commit66f8363254cf23e283186e89bf815e0843a66e6b
authorNiklas Larsson <metaniklas@gmail.com>
dateSun 5 Aug 2018, 00:08 (8 years ago)
parentef155c262695fc
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)