https://github.com/EasyCrypt/easycrypt
Tip revision: ce4d67413822686817f6b2176478b1c8bd68f83e authored by Pierre-Yves Strub on 30 September 2019, 15:35:43 UTC
make things compile
make things compile
Tip revision: ce4d674
IRing.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 export Int IntExtra.
require import Ring AlgTactic.
(* -------------------------------------------------------------------- *)
instance ring with int
op rzero = zero
op rone = one
op add = (+)
op opp = [-]
op mul = ( * )
op expr = IntExtra.( ^ )
proof oner_neq0 by smt
proof addr0 by smt
proof addrA by smt
proof addrC by smt
proof addrN by smt
proof mulr1 by smt
proof mulrA by smt
proof mulrC by smt
proof mulrDl by smt
proof expr0 by smt
proof exprS by smt.