on d689c19 help sign in
Idris-dev/test/interactive018
8 files
../ Imported1.idrImprove interactive018. Imported2.idrPrevent private functions showing up in autocomplete and :t. Public1.idrImprove interactive018. Public2.idrImprove interactive018. Top.idrImprove interactive018. expectedPrevent private functions showing up in autocomplete and :t. inputPrevent private functions showing up in autocomplete and :t. runPrevent private functions showing up in autocomplete and :t.