https://github.com/EasyCrypt/easycrypt
Revision c3114bd1c70ec54bde56f486f5c405a4f1f565db authored by Pierre-Yves Strub on 14 October 2020, 06:52:22 UTC, committed by Pierre-Yves Strub on 14 October 2020, 06:52:22 UTC
1 parent 4268b0f
Tip revision: c3114bd1c70ec54bde56f486f5c405a4f1f565db authored by Pierre-Yves Strub on 14 October 2020, 06:52:22 UTC
"import var" now takes a space-separated list of modules
"import var" now takes a space-separated list of modules
Tip revision: c3114bd
Bool.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require FinType.
op (^^) (b1 b2:bool) = b1 = !b2.
lemma nosmt xor_false b: b ^^ false = b
by [].
lemma nosmt xor_true b: b ^^ true = !b
by [].
lemma nosmt xorA b1 b2 b3: (b1 ^^ b2) ^^ b3 = b1 ^^ (b2 ^^ b3)
by [].
lemma nosmt xorC b1 b2: b1 ^^ b2 = b2 ^^ b1
by [].
lemma nosmt xorK b: b ^^ b = false
by [].
clone FinType as BoolFin with
type t <- bool,
op enum <- List.(::) true (List.(::) false List."[]"),
op card <- 2
proof enum_spec by case.
Computing file changes ...
