我是依赖类型的新手(尽管他们有很大的不同,我正在尝试Idris和Coq).
我试图表达以下类型:给定类型T和k nats n1,n2,… nk的序列,由k个k序列组成的类型,其长度分别为n1,… nk.
即,k个矢量的矢量,其长度由参数给出.
这可能吗?
您可以使用异构列表执行此操作,如下所示.
Require Vector. Require Import List. Import ListNotations. Inductive hlist {A : Type} (B : A -> Type) : list A -> Type := | hnil : hlist B [] | hcons : forall a l,B a -> hlist B l -> hlist B (a :: l). DeFinition vector_of_vectors (T : Type) (l : list nat) : Type := hlist (Vector.t T) l.
然后,如果l是您的长度列表,则类型vector_of_vectors将使用您描述的类型.
例如,我们可以构造一个vector_of_vectors bool的元素[2; 0; 1]:
Section example. DeFinition ls : list nat := [2; 0; 1]. DeFinition v : vector_of_vectors bool ls := hcons [false; true] (hcons [] (hcons [true] hnil)). End example.
此示例对您可以设置的向量使用一些符号:
Arguments hnil {_ _}. Arguments hcons {_ _ _ _} _ _. Arguments Vector.nil {_}. Arguments Vector.cons {_} _ {_} _. Delimit Scope vector with vector. Bind Scope vector with Vector.t. Notation "[ ]" := (@Vector.nil _) : vector. Notation "a :: v" := (@Vector.cons _ a _ v) : vector. Notation " [ x ] " := (Vector.cons x Vector.nil) : vector. Notation " [ x ; y ; .. ; z ] " := (Vector.cons x (Vector.cons y .. (Vector.cons z Vector.nil) ..)) : vector. Open Scope vector.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。