Matita Home

`inline "s" params`

- Synopsis:
**inline***qstring**inline_params*- Action:
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 |