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
最新問題