idris-community / inigo

Inigo: A Package Manager for Idris2
https://inigo.pm
MIT License
61 stars 7 forks source link

lambdaRequire has been removed from Idris 2 #7

Closed michaelmesser closed 3 years ago

michaelmesser commented 3 years ago

https://github.com/idris-community/inigo/blob/1d05cea0b0a45d9728514150f97f8b8f1c2ba9c9/Inigo/Async/Util.idr#L19 See https://github.com/idris-lang/Idris2/pull/873

hayesgm commented 3 years ago

Thanks-- will work on updating this.

andylokandy commented 3 years ago

This should be fixed by https://github.com/idris-community/inigo/pull/9

hayesgm commented 3 years ago

Thanks