https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: c44174dfe2349167774459e3b28424f99a6b8fcb authored by Christian Doczkal on 08 December 2021, 16:20:51 UTC
eager random oracle for unit domain (single random variable)
Tip revision: c44174d
ecWhy3Conv.mli
(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
open Why3

module Talpha : sig
  type t = Term.vsymbol list * Term.term

  val compare : t -> t -> int
end

module Mta : EcMaps.Map.S with type   key = Talpha.t
module Sta : EcMaps.Set.S with type M.key = Talpha.t
back to top