inline "s" params


inline qstring inline_params


Inlines a representation of the item s, which can be the URI of a HELM object. If an entire HELM directory (i.e. a base URI) or the path of a *.ma source file is provided, all the contained objects are represented in a row. If the inlined object has a proof, this proof is represented in several ways depending on the provided parameters.


Table 9.2. inline-params

Table 9.3. inline-param

inline_param::=axiomTry to give an axiom flavour (bodies are omitted even if present)
 |definitionTry give a definition flavour
 |theoremTry give a theorem flavour
 |lemmaTry give a lemma flavour
 |remarkTry give a remark flavour
 |factTry give a fact flavour
 |variantTry give a variant flavour (implies plain)
 |declarativeRepresent proofs using declarative tactics (this is the dafault and can be omitted)
 |proceduralRepresent proofs using procedural tactics
 |plainRepresent proofs using plain proof terms
 |nodefaults Do not use the tactics depending on the default command (rewrite in the procedural mode)
 |level=nat Set the level of the procedural proof representation (the default is the highest level)