https://github.com/EasyCrypt/easycrypt
Revision 3ffc3beb6838ddcc61710a1327ef58b4714fce53 authored by Alley Stoughton on 06 October 2021, 15:00:49 UTC, committed by Pierre-Yves Strub on 07 October 2021, 06:39:26 UTC
floor x and ceil x.
1 parent 0656ac7
Tip revision: 3ffc3beb6838ddcc61710a1327ef58b4714fce53 authored by Alley Stoughton on 06 October 2021, 15:00:49 UTC
Some lemmas for floor and ceil, in particular letting one rewrite
Some lemmas for floor and ceil, in particular letting one rewrite
Tip revision: 3ffc3be
ecUid.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 EcMaps
open EcSymbols
(* -------------------------------------------------------------------- *)
val unique : unit -> int
(* -------------------------------------------------------------------- *)
type uid = int
type uidmap
val create : unit -> uidmap
val lookup : uidmap -> symbol -> uid option
val forsym : uidmap -> symbol -> uid
(* -------------------------------------------------------------------- *)
val uid_equal : uid -> uid -> bool
val uid_compare : uid -> uid -> int
module Muid : Map.S with type key = uid
module Suid : Set.S with module M = Map.MakeBase(Muid)
(* -------------------------------------------------------------------- *)
module NameGen : sig
type t
val ofint : int -> string
val bulk : ?fmt:(string -> string) -> int -> string list
val create : unit -> t
val get : t -> uid -> string
end
Computing file changes ...