[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] 'divides' definition
How can I use 'use' or 'lemma' to introduce an instance of the
'divides' definition from theory divides in the prelude? I've tried
(lemma divides (n "L" m "L")) and
(lemma divides (n "L"))
and some others and was given the message:
"Found 2 resolutions for divides relative to the substitution.
Please check substitution, provide actual parameters for lemma
name, or supply more substitutions."