[Agda] Bin._<_

[James Deikun]

On Thu, 2012-08-02 at 17:04 +0400, Serge D. Mechveliani wrote:
> People,
> I have a beginner question. Probably, it is on usage of  lib-0.6.
> 
> Please, what stands for "<" for Bin  (binary naturals) ?
> I need to test a binary variant for `length' and `lookup':

You really have about 5 options here:

1) Use qualified prefix syntax:

   open import Data.Nat
   open import Data.Bin as Bin

   [later ...] Bin._<_ a b

2) Use qualified infix syntax (only on darcs Agda, not 2.3.x):

   open import Data.Nat
   open import Data.Bin as Bin

   [later ...] a Bin.< b

3) Rename Data.Bin._<_ on import:

   open import Data.Nat
   open import Data.Bin renaming (_<_ to _B<_)

   [later ...] a B< b

4) Rename Data.Nat._<_ on import:

   open import Data.Nat renaming (_<_ to _N<_)
   open import Data.Bin

   [later ...] a < b

5) Use instance arguments to overload _<_ (this may hurt a bit ...):

   open import Level using (_⊔_)
   open import Data.Nat hiding (_<_; _⊔_)
   import      Data.Nat.Properties
   open import Data.Bin hiding (_<_)
   open import Relation.Binary

   -- necessary because there's nothing between IsStrictTotalOrder
   --   and StrictTotalOrder in the standard library
   -- maybe there's something like this in the Agda Prelude already?
   record Ord {a} (Carrier : Set a) (b c : _)
             : Set (a ⊔ Level.suc b ⊔ Level.suc c) where
     constructor ord
     field
       {_≈_} : Rel Carrier b
       {_<_} : Rel Carrier c
       isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
     open IsStrictTotalOrder isStrictTotalOrder public

   mkOrd : forall    {a b c} (sto : StrictTotalOrder a b c) 
                  -> Ord (StrictTotalOrder.Carrier sto) b c
   mkOrd sto = ord (StrictTotalOrder.isStrictTotalOrder sto)

   open Ord {{...}}

   -- introducing instances into scope
   ordNat = mkOrd Data.Nat.Properties.strictTotalOrder
   ordBin = mkOrd Data.Bin.strictTotalOrder

If you're going to be doing (5) a lot you probably want to make Ord
into its own module or depend on a library like the Agda prelude.

(BTW Andreas or anybody who knows -- why can't the level of Ord be
inferred?)