on 7d42ba2 help sign in
Idris-dev/test/records002
3 files
../ expectedRename record002 test to the correct name! record002.idrChanged tests for new record syntax. runRename record002 test to the correct name!