Closed ohad closed 3 years ago
(user-name structure introduced here: https://github.com/idris-lang/Idris2/pull/1926 )
(user-name structure introduced here: https://github.com/idris-lang/Idris2/pull/1926 )