The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 09/05/2012 16:19, AUGER Cédric a écrit :
> Of course, you can use:
> Inductive val : Type :=
>   | vnat : nat → val
>   | varray (head : val) (tail : list val) : val
> .
> 
> Inductive val2 : Type :=
>   | vnat2 : nat → val2
>   | varray2 (l : list val) : length l > 0 → val2
> .
> [...]

Alternatively, you can use:

  Inductive rval : Type :=
     | rvnat : nat -> rval
     | rvarray : list rval -> rval.

  Fixpoint rval_ok x :=
    match x with
      | rvnat _ => true
      | rvarray xs =>
          match xs with
            | nil => false
            | _ => forallb rval_ok xs
          end
    end.

  Definition val := { x : rval | rval_ok x = true }.

And then define vnat and varray (and inductive principles) with the
types you want. There is (much) more boilerplate than Cédric's
proposition, but I feel this way of translating is more generic.
Moreover, you have a canonical representation, the coercion from val to
rval is just a projection, and only type rval would survive after
extraction.


Cheers,

-- 
Stéphane