search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

Implement coercion between path types and function types #266

Closed valis closed 3 years ago

valis commented 4 years ago

Elements of Path A a a' can be coerced to and from the type of functions \Pi (i : I) -> A i.

ice1000 commented 4 years ago

Duplicate of #221 I guess

ice1000 commented 4 years ago

No, it's not.