Skip to content

The Tortoise and the Hare in Coq. Constructive extraction via Bar inductive predicates (see README.md below).

Notifications You must be signed in to change notification settings

DmxLarchey/The-Tortoise-and-the-Hare

Repository files navigation

The Tortoise and the Hare in Coq

    (**************************************************************)
    (*   Copyright Dominique Larchey-Wendling [*]                 *)
    (*                                                            *)
    (*                             [*] Affiliation LORIA -- CNRS  *)
    (**************************************************************)
    (*      This file is distributed under the terms of the       *)
    (*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
    (**************************************************************)

What is this repository for

How do I set it up

  • Use Coq 8.6 (preferably). The code also compiles with Coq 8.5pl[23]. But not under Coq 8.7 (see below).
  • To compile, type make all. Then one can visit the individual proof files *.v
  • Beware that Extraction will fail with Coq 8.7+ because Require Extraction should be included before extraction takes place. This is an unfortunate incompatibility introduced in Coq 8.7.
  • If using Coq 8.7 is nonetheless important, the rest of the code should work ok, so simply add Require Extraction where it is needed.

About

The Tortoise and the Hare in Coq. Constructive extraction via Bar inductive predicates (see README.md below).

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published