[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]


In chunnel.pvs I have, for instance, a theory 'points' which defines a type 
'points_value' and an assumption on this type 'points_ax'. In the theory 
'Thedford_scenario' a constant 'mp' of type 'points_value' is declared and 
instantiated. I thought that this would then incur an obligation to prove the 
assumption 'points_ax'. However, on doing a typecheck no such tcc occurs. Why is 
this? Is there any other way to write this so that the relevant tcc's occur?