agda - how to define an element of type record? -

i have define datatype of real number as..

record ℝ : set    field        l : stream pair       r : stream pair       inhabited : ∀ (x : pair) → ( (x mem l) or (x mem r))        disjoint    : ∀ (x : pair) → ( (not (x mem l)) or (not (x mem r)))        located     : ∀ (x y : pair) → (x ≤pair y) → ((x mem l) or (y mem r))   

now want define element of type r . tried as..

mkreal : stream pair -> stream pair -> r mkreal x y = record { l = x; r = y}.  

but not working please help.

your record ℝ has 5 fields, l, r, inhabited, disjoint, , located. define instance of ℝ, have supply values 5 fields:

mkreal x y = record { l = x; r = y; inhabited = ?; disjoint = ?; located = ? } 

you have pass values of inhabited, disjoint, , located arguments mkreal well.

by way, there way automatically define constructor record:

record ℝ : set    constructor mkreal    field        l : stream pair       r : stream pair       inhabited : ∀ (x : pair) → ((x mem l) or (x mem r))        disjoint    : ∀ (x : pair) → ((not (x mem l)) or (not (x mem r)))        located     : ∀ (x y : pair) → (x ≤pair y) → ((x mem l) or (y mem r))   

as bonus, can use mkreal when pattern matching:

foo : ℝ → ? foo (mkreal l r inhabited disjoint located) = ?