Logic.Judge.Formula

Re-export of the Formula datastructure, including class instances.

Documentation

module Logic.Judge.Formula.Datastructure

module Logic.Judge.Formula.Parser

class (Eq e, Ord e, Parseable e, Subterm e e, HasVariables e, Substitutable e e) => Extension e

Any extension of logical formulas is parseable, its extension terms are subterms of its formulas, and they can be substituted into.

This encompassing class shortens class constraints and also avoids UndecidableInstances in some cases.

Instances

Extension Justification