Project

General

Profile

Revision 4d841db7

View differences:

include/lustrec_math.lusi
23 23
function sqrt (x: real) returns (y: real) prototype C lib m;
24 24
function trunc (x: real) returns (y: real) prototype C lib m;
25 25
function tan (x: real) returns (y: real) prototype C lib m;
26

  
26
function tanh (x: real) returns (y: real) prototype C lib m;
include/lustrec_math.smt2
23 23
(declare-rel exp ( Real Real) )
24 24
(declare-rel log ( Real Real) )
25 25
(declare-rel log10 ( Real Real) )
26
(declare-rel tanh ( Real Real) )

Also available in: Unified diff