I’d really like to
From Coq.Vectors Require Import Fin (fin := t).
From Coq Require Import Vector
Check fin. (* nat -> Set *)
Check t. (* Type -> nat -> Type *)
The top line is my made-up syntax that I think conveys the idea. The intuition is python’s from numpy import random as ran.
How can I accomplish this?
This is a feature that has been requested before. [request] Coq selective/filtered import should support blacklists · Issue #15017 · coq/coq · GitHub for a recent example.
The type of t doesn’t quite look right to me there.
If you want to use Fin, the best way is to only Require it. I.e. From Coq.Vectors Require Fin. Then you can write Fin.t. If you still want to use fin you can declare an abbreviation:
Notation fin := Fin.t.
This would definitely be a great feature to have. Another workaround is to assign a module to a local module so you can use then in a shorter notation. but this is definitely not ideal.