Otter

Documentation

module Otter.Rule

module Otter.SearchRes

class Subsumable n where

Methods

subsumes :: n -> n -> Bool

Instances

(Ord a, Ord l) => Subsumable (LSequent a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

subsumes :: LSequent a l -> LSequent a l -> Bool

Subsumable s => Subsumable (tm ::: s)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

subsumes :: (tm ::: s) -> (tm ::: s) -> Bool

(Ord a, Ord l) => Subsumable (GoalNSequent a l)

Defined in Zsyntax.Labelled.Rule.Frontier

Methods

subsumes :: GoalNSequent a l -> GoalNSequent a l -> Bool

search :: Subsumable s => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])