Tip.Passes

Running passes in the Fresh monad

freshPass

Simplifications

simplifyTheory

gently

aggressively

data SimplifyOpts a

removeNewtype

uncurryTheory

Simplifyng conjectures

splitConjecture

skolemiseConjecture

skolemiseConjecture'

skolemise

negateConjecture

typeSkolemConjecture

intToNat

sortsToNat

Changing status of conjectures

makeConjecture

selectConjecture

provedConjecture

deleteConjecture

Boolean builtins

ifToBoolOp

boolOpToIf

theoryBoolOpToIf

removeBuiltinBool

boolOpLift

Match expressions

addMatch

commuteMatch

removeMatch

cseMatch

cseMatchNormal

cseMatchWhy3

fillInCases

Duplicated functions

collapseEqual

removeAliases

Lambda and let lifting

lambdaLift

letLift

axiomatizeLambdas

Function definitions

axiomatizeFuncdefs

axiomatizeFuncdefs2

Data types

axiomatizeDatadecls

Monomorphisation

monomorphise

Induction

induction

Miscellaneous

uniqLocals

dropSuffix

Building pass pipelines

data StandardPass

class Pass p

unitPass

lintMany

runPassLinted

data Choice a b

choice

runPasses

continuePasses

parsePasses