Matita HomeMatita Homeinline "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.3. inline-param
| inline_param | ::= | axiom | Try to give an axiom flavour (bodies are omitted even if present) |
| | | definition | Try give a definition flavour | |
| | | theorem | Try give a theorem flavour | |
| | | lemma | Try give a lemma flavour | |
| | | remark | Try give a remark flavour | |
| | | fact | Try give a fact flavour | |
| | | variant | Try give a variant flavour (implies plain) | |
| | | declarative | Represent proofs using declarative tactics (this is the dafault and can be omitted) | |
| | | procedural | Represent proofs using procedural tactics | |
| | | plain | Represent 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) | |
| | | depth=nat | TODO |