No error reported about wrong use of `\use \coerce`
Open
bug
- Dominant language
- Java
- Stars
- 756
- Forks
- 31
- PR merge metrics
- No merged PRs in 30d
Description
```
\instance FreeMonoidConstr (S : \Set) : Monoid \cowith
| E => List S
| ide => nil
| * (a1 : List S) (a2 : List S) => a1 ++ a2
| ide-left => idp
| ide-right => ++_nil
| *-assoc => ++-assoc
\use \coerce letter {S : \Set} (s : S) : FreeMonoidConstr S => s :: nil
```
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.