5 search results for "tag:"category: Miscellaneous/Coq Use Examples""

Showing 1 - 5
  1. coq-coinductive-examples

    No documentation

    Some simple examples about co-inductive types and co-induction
    keyword: co-inductive types keyword: co-induction category: Miscellaneous/Coq Use Examples
    Eduardo Giménez
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  2. coq-cours-de-coq

    No documentation

    Various examples of Coq proofs
    category: Miscellaneous/Coq Use Examples
    Frédéric Prost Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  3. coq-demos

    No documentation

    Demos of some Coq tools appeared in version V6.0
    keyword: sorting keyword: Cases keyword: Tauto keyword: AutoRewrite keyword: Prolog category: Miscellaneous/Coq Use Examples
    Coq group
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-groups

    No documentation

    An exercise on groups
    keyword: group theory category: Miscellaneous/Coq Use Examples
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  5. coq-historical-examples

    No documentation

    Historical examples developed in the (pure) Calculus of Constructions
    keyword: Newman's lemma keyword: Tarski's fixpoint theorem keyword: line formatting keyword: binary-search paradigm keyword: square root approximation keyword: Calculus of Constructions keyword: history of Coq category: Miscellaneous/Coq Use Examples
    Gérard Huet Christine Paulin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019