https://github.com/EasyCrypt/easycrypt
Tip revision: e15c19fa91bfeaa48aac1e1225d26b3c2e38afba authored by Pierre-Yves Strub on 10 July 2019, 05:57:29 UTC
Merge branch '1.0' into deploy-transeq
Merge branch '1.0' into deploy-transeq
Tip revision: e15c19f
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.