coq

    3热度

    1回答

    Ltac：从名称

    获取假名'类型 我正在寻找一种通过它的名字获得假名以匹配它的方法。就像这样： Ltac mytactic h_name := let h := hyp_from_name h_name in match h with | _ /\ _ => do_something | _ => print_error_message end . 这将是像这样使用：
    pattern-matching coq ltac 2017-06-29

    0热度

    1回答

    在勒柯克，如何构建“SIG”型

    的元素，类型为A的一个简单的归纳定义： Inductive A: Set := mkA : nat-> A. (*get ID of A*) Function getId (a: A) : nat := match a with mkA n => n end. 和子类型的定义： (* filter that test ID of *A* is 0 *) Function filter
    types casting coq subtype 2017-07-07

    1热度

    1回答

    Idris是否支持展开函数定义？

    对于从属类型，它可以定义一个感应式的有序列表，例如： data IsSorted : {a: Type} -> (ltRel: (a -> a -> Type)) -> List a -> Type where IsSortedZero : IsSorted {a=a} ltRel Nil IsSortedOne : (x: a) -> IsSorted ltRel [x]
    coq dependent-type idris type-theory 2017-07-07

    1热度

    1回答

    证明共同自然数的coinduction原理

    我不得不承认，我不是很擅长coinduction。我试图在共自然数上展示一个互模拟原则，但我被困在一对（对称）情况下。 CoInductive conat := | cozero : conat | cosucc : conat -> conat. CoInductive conat_eq : conat -> conat -> Prop := | eqbase
    coq coq-tactic coinduction 2017-07-10

    2热度

    1回答

    平等的勒柯克

    SIG类型的元素随着SIG类型确定指标，如： Inductive A: Set := mkA : nat-> A. Function getId (a: A) : nat := match a with mkA n => n end. Function filter (a: A) : bool := if (beq_nat (getId a) 0) then true else false.
    coq subtype 2017-07-10

    1热度

    1回答

    Coq如何定位并转换假设以表明它们是假的？

    我试图证明，如果两个布尔表的列表是相等的（使用一个相等的定义，以明显的方式在结构上列出结构列表），那么它们具有相同的长度。然而，在这样做的过程中，我最终处于一种错误/无人居住的假设，但不是字面上的False（因此不能以contradiction策略为目标）。 这是我到目前为止。 Require Import Coq.Lists.List. Require Export Coq.Bool.Bool
    coq 2017-07-11

    2热度

    1回答

    Coq：设置默认隐式参数

    假设我有一个包含很多模块和部分的代码。其中一些有多态的定义。 Module MyModule. Section MyDefs. (* Implicit. *) Context {T: Type}. Inductive myIndType: Type := | C : T -> myIndType. End MyDefs.
    implicit coq 2017-07-12

    0热度

    1回答

    Coqc mangles文件名

    每当我从终端呼叫coqc A或coqc A.v，我得到错误Error: Can't find file A.v.v on loadpath（注意双.v.v）。这是在Mac OS上通过Opam全新安装的Coq 8.6（我以前使用8.4和8.5时没有麻烦）。 有什么建议吗？
    coq 2017-07-13

    6热度

    2回答

    提高coq策略的失败水平

    当在Ltac中实现复杂的策略时，我预计会出现一些Ltac命令或战术调用失败以及预期的位置（例如终止repeat或导致回溯）。这些故障通常在故障级别为0时提升。 故障在较高级别上升“逃脱”周围的try或repeat区块，并可用于发出意外故障。 我缺少的是什么，甚至为0级运行策略tac和对待它的失败，是在一个较高的水平，同时保留了失败的消息的方式。这可以让我确保repeat不会由于我身边的Ltac编程
    coq coq-tactic ltac 2017-07-14

    1热度

    1回答

    Coq：导入关于实例的信息

    Section Definitions. Definition eq_dec X := forall x y : X, {x=y} + {x <> y}. Existing Class eq_dec. (* Any function that uses eq_dec. Doesn't matter -- ↓ ↓ ↓ *) Definition f {X:
    typeclass implicit coq 2017-07-17
最新问题