blob: f5d0d1a5230917b7bf750e1da02f4bf646ee2213 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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.
|
