Commit 54c1d687 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Mise en commentaire des fichiers de parsing et débuts d'ajout de preuves dans Mix.v et Peano.v

parent 9368d515
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v parser.v FormulaReader.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......@@ -34,13 +34,13 @@ COQMF_CMDLINE_COQLIBS =
# #
###############################################################################
COQMF_LOCAL=1
COQMF_COQLIB=/home/letouzey/V8//
COQMF_DOCDIR=/home/letouzey/V8/doc/
COQMF_OCAMLFIND=/usr/bin/ocamlfind
COQMF_CAMLP5O=/usr/bin/camlp5o
COQMF_CAMLP5BIN=/usr/bin/
COQMF_CAMLP5LIB=/usr/lib/ocaml/camlp5
COQMF_LOCAL=0
COQMF_COQLIB=/home/samuel/.opam/system/lib/coq/
COQMF_DOCDIR=/home/samuel/.opam/system/doc/
COQMF_OCAMLFIND=/home/samuel/.opam/system/bin/ocamlfind
COQMF_CAMLP5O=/home/samuel/.opam/system/bin/camlp5o
COQMF_CAMLP5BIN=/home/samuel/.opam/system/bin/
COQMF_CAMLP5LIB=/home/samuel/.opam/system/lib/camlp5
COQMF_CAMLP5OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59 -safe-string
COQMF_HASNATDYNLINK=true
......
......@@ -11,7 +11,6 @@ Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope string_scope.
Local Open Scope eqb_scope.
(** We use here a Locally nameless representation of terms.
See for instance http://www.chargueraud.org/research/2009/ln/main.pdf
*)
......
......@@ -96,6 +96,14 @@ Qed.
End PeanoAx.
Local Open Scope string.
Local Open Scope formula_scope.
(** Some basic proofs in Peano arithmetics. *)
Lemma Comm : Pr intuiti (∀∀ (#0 + #1 = #1 + #0)).
Proof.
Qed.
Definition PeanoTheory :=
{| sign := PeanoSign;
......
......@@ -19,5 +19,5 @@ Theories.v
PreModels.v
Models.v
Peano.v
parser.v
FormulaReader.v
# parser.v
# FormulaReader.v
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment