(* Listen können folgendermaßen definiert werden *)

Section Lists.

Variable A: Set.
Set Implicit Arguments.

Inductive my_list: Set :=
   nil : my_list    |    cons: A -> my_list -> my_list.

End Lists.

Check my_list_ind.

Check my_list_rect.
Print my_list_rect.

(* Natürlich gibt es diesen Datentyp auch in der Standardbibliothek *)
(* Das entsprechende Modul wird folgendermaßen geladen *)

Require Import List.

(* Es führt die folgenden Notationen ein: *)
(* cons a u = a :: u, für das Einfügen vorne *)
(* app u v = u ++ v,  für die Listenverkettung *)

(* Beispiel: *)
Eval compute in
    (1::2::3::nil) ++ (7::8::nil).

(* Das Induktions- (bzw. Rekursions-)prinzip ist so wie oben. *)
Check list_ind.
Check list_rect.

(* Besser als eine Direkte Anwendung von list_rect, ist *)
(* es, Funktionen durch Gleichungen zu definieren: *)

Check list nat.

(* Beispiel: Hintenanfügen *)
Section Add.
Variable A: Set.
Fixpoint add  (u: list A) (b:A) {struct u}: list A :=
   match u with
   | nil => b :: nil
   | a::v => a:: (add v b)
end.

Check add.
Print add.

End Add.

(* Außerhalb des obigen Kontexts, wird die Abhängigkeit *)
(* vom Alphabet A explizit angegeben: *)
Print add.

Eval compute in
    add (1::2::3::nil)  7.

(* Die Funktion rev kehrt die Reihenfolge um: *)

Eval compute in
    rev (1::2::3::4::nil).

Print rev.


Infix "⊲" := cons (at level 60, right associativity) : list_scope.

Open Scope list_scope.
Implicit Arguments nil [A].
Print nil.
Open Scope list_scope.
Check 3 ⊲ nil.