https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecAlgTactic.mli
(* --------------------------------------------------------------------
* 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-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcTypes
open EcDecl
open EcFol
open EcAlgebra
open EcCoreGoal
(* -------------------------------------------------------------------- *)
val is_module_loaded : EcEnv.env -> bool
(* -------------------------------------------------------------------- *)
val ring_symbols : EcEnv.env -> EcDecl.rkind -> ty -> (symbol * (bool * ty)) list
val field_symbols : EcEnv.env -> ty -> (symbol * (bool * ty)) list
val ring_axioms : EcEnv.env -> ring -> (symbol * form) list
val field_axioms : EcEnv.env -> field -> (symbol * form) list
(* -------------------------------------------------------------------- *)
val t_ring : ring -> eq list -> form * form -> FApi.backward
val t_ring_simplify : ring -> eq list -> form * form -> FApi.backward
val t_ring_congr :
cring -> RState.rstate -> int list -> form list -> FApi.backward
(* -------------------------------------------------------------------- *)
val t_field : field -> eq list -> form * form -> FApi.backward
val t_field_simplify : field -> eq list -> form * form -> FApi.backward
val t_field_congr :
cfield -> RState.rstate -> int list -> form list -> FApi.backward
