--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Maybe I should have been more clear. I'm familiar with the fact that there are many proof assistants with declarative syntax out there; I was specifically asking if anyone has tried implementing such a syntax "at user level" using mixfix binders.