Transformation `apply` and inductive predicates
The apply transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unitapply 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