Agda-2.2.10: A dependently typed functional programming language and proof assistantContentsIndex
ABCDEFGHIJKLMNOPQRSTUVWXYZ:!$&+./<=>|-
Index (B)
B
Backend
backupPos
BadImplicits
begin
beginningOf
beginningOfFile
begin_
betareduce
between
BinAppView
binAppView
Bind
bindAsPatterns
bindBuiltin
bindBuiltinBool
bindBuiltinCons
bindBuiltinDummyConstructor
bindBuiltinEquality
bindBuiltinFlat
bindBuiltinInf
bindBuiltinLevelSuc
bindBuiltinLevelZero
bindBuiltinName
bindBuiltinNil
bindBuiltinPrimitive
bindBuiltinRefl
bindBuiltinSharp
bindBuiltinSuc
bindBuiltinSuc'
bindBuiltinType
bindBuiltinType1
bindBuiltinZero
bindBuiltinZero'
bindConstructor
BindHole
bindLHSVars
bindModule
bindName
bindParameters
bindPostulate
bindPostulatedName
bindPrimitive
bindQModule
bindToConcrete
bindVariable
binop
Blind
1 (Data Constructor)
2 (Type/Class)
BlkInfo
Block
Blocked
1 (Data Constructor)
2 (Type/Class)
3 (Data Constructor)
blocked
BlockedConst
BlockedLevel
blockingMeta
blockOfLines
blockTerm
bltQual
bltQual'
BName
bnameFixity
Body
bol
boolPrimTF
boolSemiring
BothWithAndRHS
Bound
BoundName
boundName
braces
1 (Function)
2 (Function)
braces'
bracket
brackets
1 (Function)
2 (Function)
Branch
1 (Type/Class)
2 (Data Constructor)
Branches
brExpr
BrInt
brInt
brName
brTag
brVars
buildClosure
buildConstraint
buildGraph
buildInterface
buildList
buildMPatterns
buildOccurrenceGraph
buildWithFunction
Builtin
1 (Type/Class)
2 (Data Constructor)
builtinAgdaTerm
builtinAgdaTermCon
builtinAgdaTermDef
builtinAgdaTermLam
builtinAgdaTermPi
builtinAgdaTermSort
builtinAgdaTermUnsupported
builtinAgdaTermVar
builtinArg
builtinArgArg
builtinBool
builtinChar
builtinCons
builtinConstructors
builtinDatatypes
builtinEquality
builtinFalse
builtinFlat
builtinFloat
builtinInf
BuiltinInParameterisedModule
builtinInteger
builtinIO
builtinLevel
builtinLevelKit
builtinLevelMax
builtinLevelSuc
builtinLevelZero
builtinList
BuiltinMustBeConstructor
builtinNat
builtinNatDivSucAux
builtinNatEquals
builtinNatLess
builtinNatMinus
builtinNatModSucAux
builtinNatPlus
builtinNatTimes
builtinNil
builtinPostulates
BuiltinPragma
1 (Data Constructor)
2 (Data Constructor)
builtinPrimitives
builtinQName
builtinRefl
builtinSharp
builtinSize
builtinSizeInf
builtinSizeSuc
builtinString
builtinSuc
BuiltinThings
builtinTrue
builtinTypes
builtinZero