on master 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. expected.outRename expected, input and run input.inRename expected, input and run run.shRename expected, input and run