# PVS Bug 1009

Synopsis: PVS 4.1 M-x tc --> Error: No methods applicable for generic function
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: open
Class: sw-bug
Arrival-Date: Thu Nov 8 14:50:00 2007
Originator: Rick Butler
Organization: larc.nasa.gov
Release: PVS 4.0
Environment:
System:
Architecture:
Description:
The following theory:
vect_trig_2D: THEORY
BEGIN
IMPORTING vectors2D
u,v,w : VAR Vector
a,b,c : VAR real
cross(u,v): real = u`x*v`y - v`x*u`y
sin(u: Vector,v:{vv: Vector | norm(u) * norm(vv) /= 0}): real = cross(u,v)/
(norm(u)*norm(v))
cos(u: Vector,v:{vv: Vector | norm(u) * norm(vv) /= 0}): real = u*v/(norm(u
)*norm(v))
trig_range : TYPE = {a | -1 <= a AND a <= 1}
sin_range : JUDGEMENT sin(u,v) HAS_TYPE trig_range
cos_range : JUDGEMENT cos(u,v) HAS_TYPE trig_range
sin2_cos2: THEOREM sq(sin(u,v)) + sq(cos(u,v)) = 1
END vect_trig_2D
produces
Error: No methods applicable for generic function
when given
M-x tc
How-To-Repeat:
Fix: