関数内で暗黙の変数を使用するにはどうすればよいですか? 最も単純なケースに還元すると、次のことが可能になります。
dim : Vect n a -> Nat
dim vec = n
エラーを取得せずに:
When elaborating right hand side of rep:
No such variable n
内部から値にアクセスする方法はありますか? nそれとも中を求めるのと同じsin nですか？
Vectこの場合、それが「全単射」であることを証明し、そこから変数を復元することは可能ですか?