Module Export_why3.Make

Parameters

module T : Logic.Term

Signature

module Env : Engine.Env with type term := T.term
type trigger = ( T.var, T.Fun.t ) Engine.ftrigger
type typedef = ( T.tau, T.Field.t, T.Fun.t ) Engine.ftypedef
class virtual engine : object ... end