1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "datatypes/pairs.ma".
17 ninductive void : Type[0] ≝.
19 ninductive unit : Type[0] ≝ something: unit.
21 ninductive Sum (A,B:Type[0]) : Type[0] ≝
25 interpretation "Disjoint union" 'plus A B = (Sum A B).
27 ninductive option (A:Type[0]) : Type[0] ≝
29 | Some : A → option A.