• Rocq logo Rocq logo
  • Standard Library
  • Learn
  • Platform
  • Packages
  • Community
  • Consortium
  • News
  • Get Started
  • Rocq logo Rocq logo
  • Learn
  • Platform
  • Packages
  • Community
  • Consortium
  • News
  • Standard Library
  • Get started

3 search results for "tag:"keyword: Higman's lemma""

Showing 1 - 3
  1. coq-higman-cf

    No documentation

    A direct constructive proof of Higman's Lemma
    keyword: Higman's lemma keyword: extraction category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Stefan Berghofer
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  2. coq-higman-nw

    No documentation

    A program from an A-translated impredicative proof of Higman's Lemma
    keyword: A-translation keyword: Higman's lemma keyword: impredicativity keyword: System F keyword: extraction category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Hugo Herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  3. coq-higman-s

    No documentation

    Higman's lemma on an unrestricted alphabet
    keyword: Higman's lemma keyword: well quasi-ordering category: Mathematics/Combinatorics and Graph Theory date: 2007-09-14
    William Delobel <william.delobel@lif.univ-mrs.fr>
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019

Footer

Rocq Rocq

Interactive Theorem Prover

Zulip GitHub Discourse Mastodon RSS
GitHub branch and commit.

About Rocq

  • Changelog
  • Releases
  • Industrial Users
  • Academic Users
  • History
  • Why Rocq?
  • Roadmap

Resources

  • Install Rocq
  • Get Started
  • Documentation
  • Books
  • Papers
  • Logo

Ecosystem

  • Platform
  • Packages
  • Rocq Team
  • Community
  • Consortium
  • Events
  • Rocq Planet
  • Jobs

Policies

  • Governance
  • Privacy
  • Code of Conduct