Uses Coq 8.17.0 and its standard libraries enabling classical mathematical reasoning

Instructions:

gunzip coq.tar.gz ; tar xvf coq.tar; cd coq ; make

Contents:

Oracle.v: in classical logic, every proposition or its negation holds

Sets.v, Poset.v, PPO.v, CPO.v, Ideal.v, Algebraic.v, Exp.v; Embedding.v:
infrastructure for sets, posets, PPOs, CPOs, ideals, algebraic CPOs, embeddings, and exponentials

Flifting.v: lifting a monotonic function between PPOs to a unique continuous function between respective embeddings of the PPOs

Conat.v, Option.v : infrastructure for the conat and option types

Monad.v : the reader and termination state monads

Partial.v : partial recursive functions

While.v : defining the while loop as a partial recursive function

Hoare.v : Hoare logic

LinkedList.v : the type of linked lists and its properties

Length.v : the case study about the length of linked lists.