ivor-0.1.11: Theorem proving library based on dependent type theory
Contents
Index
A
B
C
D
E
F
G
H
I
K
L
M
N
O
P
Q
R
S
T
U
V
W
>
Index (G)
generalise
Ivor.TT
GenRec
Ivor.TT
getAllDefs
Ivor.TT
getAllInductives
Ivor.TT
getAllPatternDefs
Ivor.TT
getAllTypes
Ivor.TT
getApp
Ivor.ViewTerm
, Ivor.TT
getArgTypes
Ivor.ViewTerm
, Ivor.TT
getConstructorArity
Ivor.TT
getConstructors
Ivor.TT
getConstructorTag
Ivor.TT
getContext
Ivor.Shell
getDef
Ivor.TT
getElimRule
Ivor.TT
getError
Ivor.TT
getFnArgs
Ivor.ViewTerm
, Ivor.TT
getGoal
Ivor.TT
getGoals
Ivor.TT
getInductive
Ivor.TT
getPatternDef
Ivor.TT
getReturnType
Ivor.ViewTerm
, Ivor.TT
getType
Ivor.TT
Goal
Ivor.TT
goal
Ivor.TT
GoalData
Ivor.TT
goalData
Ivor.TT
goalName
Ivor.TT
goalType
Ivor.TT