Bind notation allowing for type cast annotations of variables

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

198 stars 50 forks source link

Bind notation allowing for type cast annotations of variables #175

Closed YaZko closed 4 years ago

YaZko commented 4 years ago

Possible comfort fix for #174

As far as my notation-foo goes, I think it is necessary to use a token before the ident, and that this token cannot be the same as the quote used for binding patterns.

I used an antiquote here: sounds good to you as well @Lysxia ?

Lysxia commented 4 years ago

Looks good to me. That's also as far as my notation-foo goes. Can you also add the same to ext-lib?

YaZko commented 4 years ago

Done: https://github.com/coq-community/coq-ext-lib/pull/93