[Agda] default field values

[Sergei Meshveliani]

People,
I have a question about a  default value in a record  
in the Agda language

(I do not know, may be I am missing some simple consideration).

Consider the example:

-- 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.
With both these expressions, the programmer will have certain
difficulties with using the corresponding default value.

Try another way:

-- II -------------------------------------------------------------
record Pre-Foo {α α=} (A : Setoid α α=) : Set α
  where
  open Setoid A
  field  n    : ℕ
         a    : Carrier
         mb-b : Maybe Carrier

record Foo {α α=} (A : Setoid α α=) : Set α
  where
  open Setoid A

  field  preFoo : Pre-Foo A

  open Pre-Foo preFoo

  foo : Pre-Foo A
  foo = record { n    = n;
                 a    = a;
                 mb-b = case n ≤? 1 of \ { (yes _) → just a
                                         ; (no _)  → mb-b   }
       	       }
--------------------------------------------------------------------

Foo  takes  Pre-Foo  and updates the field  mb-b  respectively.
I doubt of whether this approach is better than (I).

It occurs that 

  one needs to program a value for  mb-b  individually for each record  
  instance,
  while is is desirable to define a default case value, and to declare 
  it as a part of the record declaration.


Consider a new syntax with a keyword `default' :

  record Foo {α α=} (A : Setoid α α=) : Set α
    where
    open Setoid A

    field  n    : ℕ
           a    : Carrier
           mb-b : Maybe Carrier        

    default                                                        
      mb-b : n ≤ 1 → Maybe Carrier    
      mb-b _ = just a   

(I doubt about the precise signature) 

-- with the meaning of a default for the field  mb-b  by the condition
n ≤ 1.

There arise the questions:

1) Can this notion be nicely expressed in the current Agda ?
2) What will happen with the language after introducing `default' ?
3) If it has sense, is it difficult to implement?

Thanks,

------
Sergei