File: bug_2353.v

package info (click to toggle)
coq 9.1.0%2Bdfsg-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 35,964 kB
  • sloc: ml: 239,908; sh: 4,355; python: 2,985; ansic: 2,644; makefile: 874; lisp: 171; javascript: 63; xml: 24; sed: 2
file content (12 lines) | stat: -rw-r--r-- 496 bytes parent folder | download | duplicates (8) 
1
2
3
4
5
6
7
8
9
10
11
12
 
(* Are recursively non-uniform params correctly treated? *)
Inductive list (A:nat -> Type) n := cons : A n -> list A (S n) -> list A n.
Inductive term n := app (l : list term n).
Definition term_list :=
  fix term_size n (t : term n) (acc : nat) {struct t} : nat :=
    match t with
    | app _ l =>
      (fix term_list_size n (l : list term n) (acc : nat) {struct l} : nat :=
      match l with
      | cons _ _ t q => term_list_size (S n) q (term_size n t acc)
      end) n l (S acc)
    end.