blob: 5257a0322aa8e0e51035ab9c0d7988e908ad5071 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Classes.RelationClasses List Setoid.
Definition RowType := list Type.
Inductive RowTypeDecidable (P : forall T, relation T) `(forall T, Equivalence (P T))
: RowType -> Type :=
| RTDecNil : RowTypeDecidable P _ nil
| RTDecCons : forall T Ts, (forall t0 t1 : T,
{P T t0 t1} + {~P T t0 t1})
-> RowTypeDecidable P _ Ts
-> RowTypeDecidable P _ (T :: Ts).
(* Toplevel input, characters 15-378:
Error:
Last occurrence of "RowTypeDecidable" must have "H" as 2nd argument in
"RowTypeDecidable P (fun T : Type => H T) nil". *)
|
