diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
commit | d5b86a98560c36fbcb3ab8d2698e09147acda512 (patch) | |
tree | f3ab850a1620fa5d3dbbe439998d09de8e0d817d /lib/Lattice.v | |
parent | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (diff) | |
parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
download | compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.tar.gz compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.zip |
Merge branch 'master' into add-file
Diffstat (limited to 'lib/Lattice.v')
-rw-r--r-- | lib/Lattice.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v index 352b4479..4455e22f 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -33,21 +33,21 @@ Local Unset Case Analysis Schemes. Module Type SEMILATTICE. - Variable t: Type. - Variable eq: t -> t -> Prop. - Hypothesis eq_refl: forall x, eq x x. - Hypothesis eq_sym: forall x y, eq x y -> eq y x. - Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Variable beq: t -> t -> bool. - Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. - Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x y, eq x y -> ge x y. - Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Variable bot: t. - Hypothesis ge_bot: forall x, ge x bot. - Variable lub: t -> t -> t. - Hypothesis ge_lub_left: forall x y, ge (lub x y) x. - Hypothesis ge_lub_right: forall x y, ge (lub x y) y. + Parameter t: Type. + Parameter eq: t -> t -> Prop. + Axiom eq_refl: forall x, eq x x. + Axiom eq_sym: forall x y, eq x y -> eq y x. + Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Parameter beq: t -> t -> bool. + Axiom beq_correct: forall x y, beq x y = true -> eq x y. + Parameter ge: t -> t -> Prop. + Axiom ge_refl: forall x y, eq x y -> ge x y. + Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. + Parameter lub: t -> t -> t. + Axiom ge_lub_left: forall x y, ge (lub x y) x. + Axiom ge_lub_right: forall x y, ge (lub x y) y. End SEMILATTICE. @@ -57,8 +57,8 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. Include Type SEMILATTICE. - Variable top: t. - Hypothesis ge_top: forall x, ge top x. + Parameter top: t. + Axiom ge_top: forall x, ge top x. End SEMILATTICE_WITH_TOP. |