- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在尝试使用“车队模式”来保留 3 个变量(两个参数和返回值)之间的依赖关系:
Require Import Vector.
(* "sparse" vector type *)
Notation svector A n := (Vector.t (option A) n).
Fixpoint svector_is_dense {A} {n} (v:svector A n) : Prop :=
match v with
| Vector.nil => True
| Vector.cons (None) _ _ => False
| Vector.cons (Some _) _ xs => svector_is_dense xs
end.
Lemma svector_tl_dense {A} {n} {v: svector A (S n)}:
svector_is_dense v -> svector_is_dense (Vector.tl v).
Admitted.
Lemma svector_hd {A} {n} (v:svector A (S n)): svector_is_dense v -> A.
Admitted.
Fixpoint vector_from_svector {A} {n} {v:svector A n} (D:svector_is_dense v): Vector.t A n :=
match n return (svector A n) -> (svector_is_dense v) -> (Vector.t A n) with
| O => fun _ _ => @Vector.nil A
| (S p) => fun v0 D0 => Vector.cons
(svector_hd v0 D0)
(vector_from_svector (Vector.tl v) (svector_tl_dense D))
end v D.
问题出现在最后一个定义中。有什么建议为什么它不起作用吗?
最佳答案
你几乎是对的。问题出在您的 return
子句中,该子句是非依赖的。你需要的是
match n return forall (w: svector A n), (svector_is_dense w) -> (Vector.t A n) with
因此 D0
不是您的情况下的 svector_is_dense v
类型,而是 svector_is_dense v0
。
顺便说一下,在第二个构造函数中,我猜你指的是 Vector.tl v0
和 svector_tl_dense D0
。这是我写的完整术语(不要介意 cons
中的附加 _
,我没有激活 implicits):
Fixpoint vector_from_svector {A} {n} {v:svector A n} (D:svector_is_dense v): Vector.t A n :=
match n return forall (w:svector A n), (svector_is_dense w) -> (Vector.t A n) with
| O => fun _ _ => @Vector.nil A
| (S p) => fun v0 D0 => Vector.cons _
(svector_hd v0 D0) _
(vector_from_svector (svector_tl_dense D0))
end v D.
关于辅 enzyme Q "convoy pattern",我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/31041297/
这个问题在这里已经有了答案: Difference between / and /* in servlet mapping url pattern (5 个回答) 4年前关闭。 web.xml 中的/
Scala 具有支持模式匹配中析取的语言功能(“模式替代”): x match { case _: String | _: Int => case _ => } 但是,如果审查满足 P
解释我的问题: 类别:玩具 特质 1:说话像男性 特质2:说话像女性 我能否在运行时更改 Toy 的行为(特征),以便有时同一个对象说话像男性,有时同一个对象说话像女性? 我想在运行时改变说话行为。
我已经能够找到很好的资源,这些资源告诉我 Java API 中的 MouseAdapter 没有使用适配器模式。问题是:MouseAdapter 是否实现了某种模式? 我知道它的作用:它为 Mouse
我有兴趣了解有关模式识别的更多信息。我知道这是一个广泛的领域,所以我将列出一些我想学习处理的特定类型的问题: 在看似随机的字节集中查找模式。 识别图像中的已知形状(例如圆形和正方形)。 注意给定位置流
关闭。这个问题需要多问focused 。目前不接受答案。 想要改进此问题吗?更新问题,使其仅关注一个问题 editing this post . 已关闭 8 年前。 Improve this ques
所以,问题很简单:在 awk 中,if (var ~/pattern/) 是否与 if (var ~ "pattern") 相同? 我已经对 csv 进行了一些基本测试,两者似乎都产生了相同的结果..
我的问题是 this 的 Scala (Java) 变体Python 上的查询。 特别是,我有一个字符串 val myStr = "Shall we meet at, let's say, 8:45
我最近一直在研究正则表达式并注意到了这一点。 Pattern pNoEmbed = Pattern.compile("[ a-z]+", Pattern.CASE_INSENSITIVE); Patt
在研究大型应用程序的 C++ 源代码时,我发现了这种模式(该示例的语法可能很粗略,但基本细节都在那里): class A : X friend B; B *parent; ...
有人可以举一个“中介者模式”在现实世界中有用的用例吗? 最佳答案 Mediator是一种添加第三方对象以控制一组(2 个或更多)对象之间交互的方法。 您能找到的最简单的示例是 Chat Room例如,
尝试编译以下代码片段时: type 'a frame = Empty | Frame of string * 'a * 'a frame let rec searchFrame f s = match
目标 我的目标是获得一个 servlet 过滤器来处理对主页的请求,然后再将它们转发到 index.jsp。 问题 我无法让过滤器接收来自“/”的请求。它的 URL 模式是 / 相反,对该模式的请求最
这个问题已经有答案了: Difference between / and /* in servlet mapping url pattern (5 个回答) 已关闭 6 年前。 我已经设置了一个具有此
第 6 章(代码重用模式)中有以下示例: // the parent constructor function Parent(name) { this.name = name || 'Adam
Pattern类中的pattern()方法和toString()方法有什么区别? 文档说: public String pattern() Returns the regular expression
我有脚本 here并且 ng-pattern 工作正常,因为 scope.subnet 仅在输入匹配模式后才显示在输出中。但是如果 ng-pattern 不匹配,ng-show 不会显示任何错误
我想知道为什么当提供相同的正则表达式和相同的字符串时,java regex pattern.matcher() 和 pattern.matches() 的结果会不同 String str = "hel
This SO answer引用“患有模式综合症的小男孩”。虽然我可以通过上下文推断出一些含义,但我并不完全理解。 “有模式综合症的小男孩”的良好定义是什么? 最佳答案 它只是意味着寻找将模式注入(i
我有以下微服务架构的用例。 我的问题是,在当前情况下,我有 3 个微服务和一个 APIGateway。 最后,网关必须在聚合(组合)来自 3 个服务的数据之前进行大量查询。因为这 3 个微服务只提供基
我是一名优秀的程序员,十分优秀!