ohtt icon indicating copy to clipboard operation
ohtt copied to clipboard

Write a script to update Notations.agda automatically

Open mikeshulman opened this issue 3 years ago • 0 comments

It would be really nice if Agda had a Reserved Notation feature like Coq, but I suppose that's impossible given its architecture.

mikeshulman avatar Jul 05 '22 20:07 mikeshulman