search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

Update typedd.rst #3307

Closed m-rinaldi closed 3 weeks ago

m-rinaldi commented 3 weeks ago

Description

System.REPL also needs to be imported in Average.idr for repl.

Should this change go in the CHANGELOG?

No