search

nunchaku-inria / nunchaku

Model finder for higher-order logic
https://nunchaku-inria.github.io/nunchaku/
BSD 2-Clause "Simplified" License
42 stars 3 forks source link

polymorphic constants #32

Open c-cube opened 5 years ago

c-cube commented 5 years ago 
val monoid: type -> type.
val inst_monoid: forall a. a -> (a -> a -> a) -> monoid a.

currently results in:

Error: ill-formed term: no quantifiers in types
  at file 'foo.nun': line 3, col 17 to 57

I suppose we should monomorphize such undefined symbols properly.