inductive void : Set \def.
-inductive Prod (A,B:Set) : Set \def
+inductive unit : Set ≝ something: unit.
+
+inductive Prod (A,B:Type) : Type \def
pair : A \to B \to Prod A B.
interpretation "Pair construction" 'pair x y =
definition sndT \def \lambda A,B:Type.\lambda p: ProdT A B.
match p with
-[(pairT a b) \Rightarrow b].
\ No newline at end of file
+[(pairT a b) \Rightarrow b].
+
+inductive option (A:Type) : Type ≝
+ None : option A
+ | Some : A → option A.
\ No newline at end of file