[Agda] default field values

[Wolfram Kahl]

On Tue, Jan 14, 2014 at 04:44:43PM +0400, Sergei Meshveliani wrote:
> -- I -----------------------------------------------------------------
> record Foo {α α=} (A : Setoid α α=) : Set α
>   where
>   open Setoid A
> 
>   field  n    : ℕ
>          a    : Carrier
> 	 mb-b : Maybe Carrier
> 
>   default-mb-b : n ≤ 1 → Maybe Carrier
>   default-mb-b _ =  just a
> 
>   mb-b-law : n ≤ 1 → Set _
>   mb-b-law _ =  mb-b ≡ just a
> ---------------------------------------------------------------------- 
> 
> I need to specify that 
>  
>   mb-b  is assigned  (just a)  for all the record instances in which 
>                                                                n ≤ 1.
> 
> The two lines of  default-mb-b  express something close to this -- but  
> not precisely.
> mb-b-law  is another attempt.

I'd say that  mb-b-law  wants to be a  field .


Wolfram