Template:Infer/doc

From Wikipedia, the free encyclopedia

This is a documentation subpage for Template:Infer (see that page for the template itself).
It contains usage information, categories and other content that is not part of the original template page.

Contents

[edit] Purpose

This template is used to draw inference figures.

[edit] Usage

{{infer
  | display = DISPLAY
  | name = NAME
  | prems = NUMBER
  | c = CONCLUSION
  | p1 = PREMISS 1
  | ...
  | p6 = PREMISS 6
}}
  • display: either block or inline (optional, default to inline)
  • name: name of the inference rule, printed after the horizontal line (optional, default to no name)
  • c: the conclusion (required)
  • prems: the number of premisses (required)
  • p1 … p6: up to six premisses. Unpredictable output if the premisses are not numbered incrementally (as many as prems required)

[edit] Examples

To write the ∧-introduction rule,

Γ ⊢ A     Γ ⊢ B  ∧I
Γ ⊢ A ∧ B

enter

{{infer
  | name = ∧I | prems = 2
  | c = Γ ⊢ ''A'' ∧ ''B''
  | p1 = Γ ⊢ ''A''
  | p2 = Γ ⊢ ''B''
}}

Arbitrary nesting is supported. For example:

⊢ p, p⊥     ⊢ q, q⊥  ⊗
⊢ p, q, p⊥ ⊗ q⊥
  		   ⊢ r, r⊥  ⊗
⊢ p, q, r, p⊥ ⊗ q⊥ ⊗ r⊥

[edit] Known bugs

  • Inline display inside tables produces unpredictable output
  • Code is brittler than talcum and uglier than sin.