Skip to main content

Browse the archive

Revision 25d7504145c07e4345a472338a8616b023fc8243 authored by Pierre-Yves Strub on 11 July 2015, 19:03:40 UTC, committed by Pierre-Yves Strub on 12 July 2015, 12:14:23 UTC 
Pretty-printing of match-fix.
 
[fix #17219]
1 parent 9b8598c
Raw File
IRing.ec 
(* --------------------------------------------------------------------
 * Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-B licence.
 * -------------------------------------------------------------------- *)

require export Int.
require import AlgTactic.
require import Ring.
instance ring with int
  op rzero = zeroz
  op rone  = onez
  op add   = (+)
  op opp   = [-]
  op mul   = ( * )
  op expr  = ( ^ )
  op sub   = (-)

  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
  proof subrE     by smt.
back to top