search

JetBrains / Arend

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

Functions in classifying expressions #203

Closed i-walker closed 4 years ago

i-walker commented 4 years ago

Somewhat related to #141 allow instance derivation to work on implicit arguments like 

{AGG : Applicative (\lam (x : \Type) => G (G x))}

This removes redundant wrappers. Also, allow instances to define those types:

\instance ListListApplicative : Applicative (\lam x => List (List x))
ice1000 commented 4 years ago

I don't think it's related to 141 but somehow #138?

i-walker commented 4 years ago

Yes, #138 relates to this issue a lot more. I haven't checked that one. Thanks for checking 😄

ice1000 commented 4 years ago

I'd close this as being duplicate of #138 -- we already talked about lambdas there.