ground_2 released and permanently renamed as ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / etc / lib / list.etc

let rec append A (l1: list A) l2 on l1 ≝
  match l1 with
  [ nil        ⇒ l2
  | cons hd tl ⇒ hd :: append A tl l2
  ].

interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).