Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

# 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:
```
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools