Transformation `apply` and inductive predicates
apply transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit goal g : unit
apply tt gives
Transformation raised a general error: apply
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information