Induction.Structural

Induction with subterms as hypotheses

subtermInduction

Case analysis (no induction hypotheses)

caseAnalysis

Obligations

data Obligation c v t

type TaggedObligation c v t

type Predicate c v

type Hypothesis c v t

Terms

data Term c v

Typing environment

type TyEnv c t

Arguments

data Arg t

Tagged (fresh) variables

data Tagged v

tag

Removing tagged variables

unTag

unTagM

unTagMapM

Linearising (pretty-printing) obligations and terms

linObligations

linObligation

linTerm

data Style c v t

strStyle

Convenience re-export

render

text