Commit 3ab15af3 authored by MARCHE Claude's avatar MARCHE Claude

fix Coq header for Parity.v

parent 931cb8e9
......@@ -14,6 +14,11 @@
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Definition even (n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
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