Macro coq

coq!() { /* proc-macro */ }

Embed coq expression inside a Rust expression. This macro takes only one argument: some raw coq code as a string literal.

While it is possible to directly write raw backend code, sometimes it can be inconvenient. For example, referencing Rust names can be a bit cumbersome: for example, the name my_crate::my_module::CONSTANT might be translated differently in a backend (e.g. in the F* backend, it will probably be My_crate.My_module.v_CONSTANT).

To facilitate this, you can write Rust names directly, using the prefix $: f $my_crate::my_module__CONSTANT + 3 will be replaced with f My_crate.My_module.v_CONSTANT + 3 in the F* backend for instance. If you want to refer to the Rust constructor Enum::Variant, you should write $$Enum::Variant (note the double dollar). If the name refers to something polymorphic, you need to signal it by adding any type informations, e.g. ${my_module::function<()>}. The curly braces are needed for such more complex expressions. You can also write Rust patterns with the $?{SYNTAX} syntax, where SYNTAX is a Rust pattern. The syntax ${EXPR} also allows any Rust expressions EXPR to be embedded. Types can be refered to with the syntax $:{TYPE}.