including

including ( <modexp> )

Imports the object specified by modexp into the current module.

See module expression for format of modexp.

Related: module expression, using, protecting, extending

`:ind { on ( ...) |

'{' on ( ...) base ( . ... .) step ( . ... .) '}'` ## {#citp-ind}

':ind on ( ...)' defines the variable for the induction tactic of CITP. ':ind { ... }' defines induction variable(s) and base pattern and step pattern specified by s.

Related: citp

Example

:ind on (M:PNat)
:ind { on (M:PNat) 
       base (<Term> . ... <Term> .) 
       step (<Term> . ... <Term> .)
     }