Tip.Core

Constructing expressions

(===)

(=/=)

neg

(/\)

(\/)

ands

ors

(==>)

(===>)

mkQuant

bool

trueExpr

falseExpr

makeIf

intLit

literal

intType

boolType

applyFunction

applySignature

apply

applyType

applyPolyType

Predicates and examinations on expressions

litView

boolView

data DeepPattern a

patternMatchingView

ifView

projAt

projGlobal

atomic

occurrences

signature

funcType

bound

locals

free

globals

tyVars

freeTyVars

exprType

builtinType

Substition and refreshing

freshLocal

freshArgs

refreshLocal

freshen

freshenNames

(//)

substMany

letExpr

unsafeSubst

Making new locals and functions

updateLocalType

updateFuncType

Matching

matchTypesIn

matchTypes

makeGlobal

Data types

constructorType

destructorType

constructor

projector

discriminator

Operations on theories

mapDecls

Topologically sorting definitions

topsort

class Definition f

data (f :+: g) a