Kai

Pattern match failure in do expression

10

`cogent -g` fails on ``` type RS s = < Continue s > type World type Array x array_bget : all x. ((Array x)!, U32) -> x type Ra =...

1. SBCL stores all proof commands in ALL CAPS; this confuses Allegro (sometimes) 2. file-targetting proof commands (`status-proof-pvs-file`, `prove-pvs-file`, etc.) finish with a message such as > PVS file pythagoras.pvs...

These trivial fixes help with getting PVS compiled on ARM-based Macs.

`powerset_finite` could be tighter

1

The prelude has ``` powerset_finite: JUDGEMENT powerset(A: finite_set[T]) HAS_TYPE finite_set[set[T]] ``` when it could be stronger. ``` powerset_finite2: JUDGEMENT powerset(A: finite_set[T]) HAS_TYPE finite_set[finite_set[T]] ``` with the proof ``` ("" (skolem-typepred)...

dump-sequent does not produce the promised `th-<theory name>.sequent` file

2

I'm chasing the cause of some proofs being tagged `incomplete`. Issuing `M-x dump-sequent` and answering `y` to the prompt doesn't produce a file (I can find). The only trace is...

I've tried two versions of table for gcd. Both render incorrectly. ``` gcd2(x,y): RECURSIVE posnat = TABLE %--------+-------------+-------------++ |[ x = y | x > y | ELSE ]| %--------+-------------+-------------++...

Declaration parameters example not working as expected

1

I've tried to cargo-cult the declaration parameter example (`groups`) from the PVS 6.0 release notes to define monotone functions: ``` mon_gen: THEORY BEGIN T[U: TYPE+]: TYPE+ FROM U poT[U: TYPE+]:...