Open
Description
Lean terms contain implicit argument info, so it should be reasonably trivial to declare it to coq
{{ message }}
No one assigned
No type
No projects
No milestone
None yet
No branches or pull requests
Lean terms contain implicit argument info, so it should be reasonably trivial to declare it to coq