首页
学习
活动
专区
工具
TVP
发布
社区首页 >问答首页 >QuickChick上下文转发

QuickChick上下文转发
EN

Stack Overflow用户
提问于 2019-06-11 02:09:04
回答 1查看 32关注 0票数 1

我对QuickChick测试框架有一个问题。假设我有一个这样的类型:

Inductive f := f1 (x : Z) (range : x < 20 /\ 0 < x).

和两个类似这样的函数:

Definition boundaries' (t : bool) :=
  if t 
  then (1, 10)%Z 
  else (10, 19)%Z .

Program Definition binary_gen (t : G bool) : G (f) :=
  bindGen ((fmap boundaries') t) (fun '(m_min, m_max) =>
    bindGen (choose (m_min, m_max)) (fun (x : Z) =>
        returnGen (f1 x _))).

当我想要证明缺少证明对象时,我有这样的上下文:

t : G bool
z, z0, x : Z
============================
x < 20 /\ 0 < x

问题是,当使用bindGen时,我需要证明当前目标,而不是之前的上下文。

因此,问题是,如何使用bindGen转发上下文,或者是否有解决此问题的方法?

EN

回答 1

Stack Overflow用户

回答已采纳

发布于 2019-06-11 03:01:17

There is a bindGen' combinator

Definition bindGen' : forall {A B : Type} (g : G A), 
                       (forall (a : A), (a \in semGen g) -> G B) -> G B.
票数 3
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/56531445

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档