convoy-pattern

    3熱度

    1回答

    依賴參數的結構遞歸

    我正試圖在Coq上寫Eratosthenes的篩子。我有一個功能crossout : forall {n:nat}, vector bool n -> nat -> vector bool n。當篩子找到一個數字是質數時，它使用crossout來標記所有不是質數的數字，然後在結果矢量上遞歸。對於矢量本身來說，篩子顯然不能在結構上遞歸，但它在矢量的長度上是結構遞歸的。我要的是做這樣的事情： Fixp
    recursion coq dependent-type convoy-pattern 2013-06-06

    3熱度

    1回答

    勒柯克「護航模式」

    我試圖用「護航模式」，保留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) : P
    coq dependent-type convoy-pattern 2015-06-25

    2熱度

    1回答

    Coq中的異構列表

    我正在考慮編寫一個Coq程序來驗證relational algebra的某些屬性。我有一些基本的數據類型工作，但連接元組給我帶來一些麻煩。 這裏是代碼的相關章節： Require Import List. Require Import String. (* An enum representing SQL types *) Inductive sqlType : Set := Nat |
    coq convoy-pattern 2015-04-02

    1熱度

    3回答

    使用來自定理的信息進行模式匹配

    我有以下問題，請查看代碼。現在 (* Suppose we have type A *) Variable A: Type. (* Also we have a function that returns the type (option A) *) Definition f_opt x: option A := ... (* Then, I can p
    pattern-matching coq dependent-type convoy-pattern 2017-06-07
最新問題