make `defs` take attributes?

[lsf37]

We often declare Haskell assertions as defs with an immediate declare x_def[simp], which is somewhat ugly.

Since defs is being defined in this repo anyway, we could just was well change its syntax and make defs [simp] legal.