gapt.examples.implicationLeftMacro
Attributes
-
Graph
-
-
Supertypes
-
class Object
trait Matchable
class Any
-
Self type
-
Members list
Iterates the implication left rule.
Iterates the implication left rule.
Value parameters
-
conclusion
-
A formula C.
-
left
-
Proofs P₁, ..., Pₙ, where pᵢ has end-sequent Γᵢ ⇒ Δᵢ, Fᵢ for i = 1, ..., n.
-
premises
-
Associates Pᵢ with Fᵢ.
-
right
-
A proof with end-sequent C, Π ⇒ Λ.
Attributes
-
Returns
-
A proof of the end-sequent F₁ → ... → Fₙ → C, Γ₁, ...,Γₙ,Π ⇒ Δ₁,...,Δₙ, Λ.