Modify syntax for properties

[yav]

It would be nice if we could write properties like this:

property
   f : [8] -> Bool
   f x = x < 10 || x >= 10

   g x = x == 0x010 || x != 0x10

Basically the syntax is that property starts a block of declarations, and all the declarations in there are properties, and type signatures are allowed. This seems much nicer than having to write:

f : [8] -> Bool
property f x = x < 10 || x >= 10

[acfoltzer]

Alternate idea @robdockins; make property a keyword that takes a list of identifiers that may be defined elsewhere (even in another module) in the usual way. E.g.,

property f, g

f : [8] -> Bool
f x = x < 10 || x >= 10

g x = x == 0x010 || x != 0x10

[brianhuffman]

One thing we might want to do is allow property to take a list of expressions rather than a list of identifiers.

A common case that I run into is that I have some properties that are size-polymorphic, which means that if I tag them with property, I can't use :prove or :check without arguments to prove/check them all at once. Instead I need to define separate identifiers for each size instance that I want to use:

foo : {n} (fin n) => [n] -> Bit
foo x = ...
property foo_1 = foo`{1}
property foo_2 = foo`{2}
property foo_3 = foo`{3}

So instead of having to invent a bunch of names for each instance, we might like to write

foo : {n} (fin n) => [n] -> Bit
foo x = ...
property foo`{1}
property foo`{2}
property foo`{3}

or even just

foo : {n} (fin n) => [n] -> Bit
foo x = ...
property foo`{1}, foo`{2}, foo`{3}