search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

[wish] :mquote:`nice <.s(foo).msg{*ugly*}>` #63

Closed gares closed 2 years ago

gares commented 2 years ago

Sometimes I want to assert a message talk about the variable X34 without quoting the entire message, eg. "coq complains variable x is illtyped"

cpitclaudel commented 2 years ago

Not sure I understand; can you give me an example of how the usage would look?

gares commented 2 years ago

maybe mquote is a misnaming and I want a massert. In the elpi tactic tutorial there are many mquote:: , but if I want to mention a part of the message inline I have to quote it all, which is too much. So Id like to assert a message really contains what I think, but show only a little fragment of it in the middle of some text explaining it.

cpitclaudel commented 2 years ago

OK, then I got it right. I have an implementation, will push soon :)

cpitclaudel commented 2 years ago

Done, check out the docs in the readme and in recipes/references.rst