This is a variant of Logitext for propositional intuitionistic logic. The calculus we have implemented is G4ip, which has the notable property that it does not need contraction to be complete. This implementation is not backed by Coq, so there may be bugs; please let me know if you find any.

Here are some examples. (Warning: some of these are impossible to prove in intuitionistic logic!)

• (A -> B) \/ (A -> C) |- A -> (B \/ C)
• A -> (B \/ C) |- (A -> B) \/ (A -> C)
• ((A -> (B -> R) -> R) -> (A -> R) -> R) -> (A -> R) -> R

Logitext/Intuitionistic is case-sensitive: capitalized identifiers represent propositions.