From c1fd2daa41aa1b915f74b4c09c6e62c79320e8ec Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 23 May 2015 16:10:16 -0400 Subject: Start implementing a Number module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The nascent Number module also serves as a proof of concept for dealing with records in the Agda standard library that are parameterized by levels instead of sets, like those in the Algebra hierarchy. These records are difficult to use as type classes, because Agda’s normal mechanism for generating type classes ('open SomeRecord ⦃...⦄') will make the levels the instance arguments, rather than the actual set the record’s functions operate on. To work around this, I defined wrapper records (effectively just named dependent pairs) parameterized in the way I desire. Each contains an underlying algebraic structure and a proof of type equality (usually just 'refl') between the parameter and the structure’s carrier. Then, I define functions over my wrapper record to rewrite with the type equality and use the underlying structure’s code. This work is related to standard library bug #35 ; fixing this bug would obviate the need for my workaround. --- B.agda | 1 + 1 file changed, 1 insertion(+) (limited to 'B.agda') diff --git a/B.agda b/B.agda index d6087d8..3e28f35 100644 --- a/B.agda +++ b/B.agda @@ -20,6 +20,7 @@ open import B.Prelude.Eq public open import B.Prelude.Functor public open import B.Prelude.List public open import B.Prelude.Maybe public +open import B.Prelude.Number public open import B.Prelude.Product public open import B.Prelude.String public open import B.Prelude.Sum public -- cgit v1.2.3