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

Re: [PVS-Help] Interpreting of "ん" as "±" (or something else?)



Ben,

This theory type-checks without problem using the patches in the github
version of the NASA PVS Library. Sam recently added the attached patch,
which may have solved the problem.

Cesar 
-- 
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 7/10/15 3:31 AM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
on behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

>exampleJapanese: THEORY
>BEGIN
>
>真(p_しません: bool): bool =
>  p_しません;
>
>しません(p_偽: bool): bool =
>  NOT (p_偽);
>
>END exampleJapanese
>

Attachment: patch-12.lisp
Description: patch-12.lisp