Skip to content

why3
why3
Opened by  

warning when cloning module containing only "val"s as abstract symbols

When cloning a module where all abstract symbols are val, like

module A0
  val f () : unit
end
module A1
  let f () = ()
  clone A0 with val f = f
end

Why3 sends the warning cloned theory .A0 does not contain any abstract symbol; it should be used instead. However, A0 does contain an abstract symbol.

Edited by Guillaume Melquiond