Tip.Core

Constructing expressions

(===)

(=/=)

oppositeQuant

gentleNeg

neg

(/\)

(\/)

ands

ors

(==>)

(===>)

mkQuant

bool

trueExpr

falseExpr

makeIf

intLit

literal

intType

boolType

applyFunction

applySignature

apply

applyTypeIn

applyType

applyTypeInExpr

applyTypeInDecl

applyPolyType

gblType

makeLets

Predicates and examinations on expressions

collectLets

litView

boolView

forallView

data DeepPattern a

patternMatchingView

ifView

projAt

projGlobal

atomic

occurrences

signature

funcType

bound

free

locals

globals

tyVars

freeTyVars

exprType

builtinType

theoryTypes

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

theoryGoals

partitionGoals

mapDecls

Topologically sorting definitions

topsort

class Definition f

data (f :+: g) a