agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

moves forward on issue #1437

Open JacquesCarette opened this issue 3 years ago • 2 comments

Renames the functions, but not the syntax.

JacquesCarette avatar Sep 29 '22 21:09 JacquesCarette

Sorry, for not replying earlier. I have replied on the issue for how to rename the syntax.

MatthewDaggitt avatar Oct 05 '22 19:10 MatthewDaggitt

Thanks - hopefully I'll have time (and wifi) on the long train ride tomorrow to deal with this.

JacquesCarette avatar Oct 05 '22 21:10 JacquesCarette

superseded now by #1916

jamesmckinna avatar Jan 25 '23 13:01 jamesmckinna