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 _ (cons 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". *)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
