File: bug_3416.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (12 lines) | stat: -rw-r--r-- 390 bytes parent folder | download | duplicates (7) 
1
2
3
4
5
6
7
8
9
10
11
12
 
Inductive list A := Node : node A -> list A
with node A := Nil | Cons : A -> list A -> node A.

Fixpoint app {A} (l1 l2 : list A) {struct l1} : list A
with app_node {A} (n1 : node A) (l2 : list A) {struct n1} : node A.
Proof.
+ destruct l1 as [n]; constructor.
  exact (app_node _ n l2).
+ destruct n1 as [|x l1].
  - destruct l2 as [n2]; exact n2.
  - exact (Cons _ x (app _ l1 l2)).
Qed.