Skip to main content

Browse the archive

Revision 7b7008967c810dab1b0766c4e299bd857a370d02 authored by François Dupressoir on 14 December 2021, 15:43:15 UTC, committed by Pierre-Yves Strub on 22 April 2022, 10:53:46 UTC 
Improve parser for anonymous proc parameters
 
Anonymous and named parameters can be mixed for abstract procedures.

Corner cases are not exercised by test suites and may crop up.

Resolves #108.
1 parent 74a4d02
Raw File
ecWhy3Conv.mli 
(* -------------------------------------------------------------------- *)
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