|
Require Import FunInd.
Require Vector.
Generalizable All Variables.
Definition f `{n:nat , u:Vector.t A n} := n.
Function f2 {A:Type} {n:nat} {v:Vector.t A n} : nat := n.
(* fails with "The reference A was not found in the current environment." *)
Function f3 `{n:nat , u:Vector.t A n} := u.
Check R_f3_complete.
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
