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?