Commit d32d2dcf authored by Heiko Becker's avatar Heiko Becker

Merge branch 'affine_arithmetic' of gitlab.mpi-sws.org:AVA/FloVer into affine_arithmetic

parents 353631d9 3e6e7f5c
Require Import Flover.CertificateChecker Flover.floverParser. Require Import Flover.CertificateChecker Flover.floverParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt. Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language Ocaml. Extraction Language OCaml.
Extraction "./binary/CoqChecker.ml" runChecker. Extraction "./binary/CoqChecker.ml" runChecker.
\ No newline at end of file
...@@ -14,7 +14,7 @@ Module OWL. ...@@ -14,7 +14,7 @@ Module OWL.
Proof. Proof.
now unfold eq; split; subst. now unfold eq; split; subst.
Qed. Qed.
Definition compare := Compare_dec.nat_compare. Definition compare := Nat.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof. Proof.
...@@ -42,8 +42,6 @@ Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity). ...@@ -42,8 +42,6 @@ Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity).
Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity). Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity).
Check (forall x S, x S -- {{x}}).
Lemma not_in_not_mem: Lemma not_in_not_mem:
forall n S, forall n S,
NatSet.mem n S = false -> NatSet.mem n S = false ->
......
#bytes:
# ocamlc -c CoqChecker.ml
# ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
native: native:
ocamlc -c big.ml ocamlc -c big.ml
ocamlc -c CoqChecker.ml ocamlc -c CoqChecker.ml
ocamlc -c CoqChecker.mli
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: native all: native
Subproject commit c25dae0a1ede617a25e49162f6f47ac9a1a2381a Subproject commit b801379405021120d0dd2b8d3a3a886c84a114a4
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