The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Hello,
any ideas of how to generalise this sequence, ie. define Tn?

Definition T0
  (A: Type)
  (f: option (A))
  :=
  { x : (A) | f  = Some x }.

Definition T1
  (A: Type)
  (B: forall (a:A), Type)
  (f: forall (a:A), option (B a))
  (a:A) :=
  { x : (B a) | f a  = Some x }.

Definition T2
  (A: Type)
  (B: forall (a:A), Type)
  (C: forall (a:A) (b: B a), Type)
  (f: forall (a:A) (b: B a), option (C a b))
  (a:A) (b: B a) :=
  { x : (C a b) | f a b  = Some x }.

Definition T3
  (A: Type)
  (B: forall (a:A), Type)
  (C: forall (a:A) (b: B a), Type)
  (D: forall (a:A) (b: B a) (c: C a b), Type)
  (f: forall (a:A) (b: B a) (c: C a b), option (D a b c))
  (a:A) (b: B a) (c: C a b) :=
  { x : (D a b c) | f a b c  = Some x }.

Thanks in advance,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France