8 search results for "tag:"category: Miscellaneous/Coq Extensions""

Showing 1 - 8
  1. coq-counting

    No documentation

    Counting: a Coq plugin for measuring definitions/proofs
    keyword: statistics category: Miscellaneous/Coq Extensions
    Stéphane Lescuyer
    8.6.0
    Unknown
    Used by 1 other packages
    20 Nov 2018
  2. coq-descente-infinie

    No documentation

    The Descente Infinie Tactic
    keyword: induction keyword: infinite descent category: Miscellaneous/Coq Extensions date: 2010-02
    Razvan Voicu <razvan@comp.nus.edu.sg> [http://www.comp.nus.edu.sg/~razvan/] Li Mengran <limengra@comp.nus.edu.sg> [http://www.comp.nus.edu.sg/~limengra]
    8.10.0
    GPL
    Used by 0 other packages
    19 Oct 2020
  3. coq-jprover

    No documentation

    A theorem prover for first-order intuitionistic logic
    keyword: decision procedure keyword: first-order logic keyword: intuitionistic logic keyword: theorem proving keyword: proof search category: Miscellaneous/Coq Extensions category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: 2002-04 (contribution since January 2009)
    Huang Guan-Shieng
    8.6.0
    Unknown
    Used by 0 other packages
    20 Nov 2018
  4. coq-maple-mode

    No documentation

    A Maple Mode for Coq
    keyword: Maple keyword: simplification keyword: field tactic category: Miscellaneous/Coq Extensions date: 2002-03
    David Delahaye Micaela Mayero
    8.9.0
    Unknown
    Used by 0 other packages
    08 Dec 2019
  5. coq-nfix

    No documentation

    Nfix: a Coq extension for fixpoints on nested inductives
    keyword: mutual fixpoint functions category: Miscellaneous/Coq Extensions
    Stéphane Lescuyer
    8.10.0
    Unknown
    Used by 0 other packages
    19 Oct 2020
  6. coq-recursive-definition

    No documentation

    ML-like recursive definitions
    keyword: recursive functions keyword: well-foundedness category: Miscellaneous/Coq Extensions date: 2002
    Antonia Balaa Yves Bertot
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    20 Nov 2018
  7. coq-reflexive-first-order

    No documentation

    Reflexive first-order proof interpreter
    keyword: computational reflection keyword: interpretation keyword: first-order logic keyword: equational reasoning category: Miscellaneous/Coq Extensions date: 2005-05
    Pierre Corbineau <pierre.corbineau@lri.fr> [http://www.cs.ru.nl/~corbineau]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  8. coq-string

    No documentation

    Definition of strings in Coq
    keyword: string keyword: ascii character category: Miscellaneous/Coq Extensions date: 2002-03
    Laurent Théry
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    20 Nov 2018