removeSkolemCongruences

gapt.proofs.expansion.removeSkolemCongruences

Attributes

Source
removeSkolemCongruences.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def remove(ep: ExpansionProof, congrs: Vector[(Expr, Expr)]): ExpansionProof

Attributes

Source
removeSkolemCongruences.scala
def repl(m: Map[Expr, Expr], et: ExpansionTree): ExpansionTree

Attributes

Source
removeSkolemCongruences.scala
def repl(m: Map[Expr, Expr], et: ETt): ETt

Attributes

Source
removeSkolemCongruences.scala
def simplCongrs(congrs: Vector[(Expr, Expr)]): Vector[(Expr, Expr)]

Attributes

Source
removeSkolemCongruences.scala