Go to the first, previous, next, last section, table of contents.

Index

Jump to: % - a - b - c - d - e - f - g - h - i - k - l - m - n - o - p - q - r - s - t - u - v - w

%

  • %abbrev
  • %assert
  • %block
  • %clause
  • %covers
  • %establish
  • %freeze
  • %infix
  • %mode, %mode
  • %name
  • %postfix
  • %prefix
  • %prove
  • %query
  • %querytabled
  • %reduces
  • %solve
  • %tabled
  • %terminates
  • %theorem
  • %total
  • %use
  • %worlds

    • a

  • abbreviations
  • add-hook
  • ambiguity
  • arguments, implicit
  • arguments, mutual
  • arithmetic
  • assumptions
  • auto-mode-alist
  • autoload

    • b

  • backquote, before variables
  • bool
  • bound variables
  • breakpoints, from Emacs

    • c

  • call patterns
  • Cartesian-closed categories
  • case, upper and lower
  • characters, reserved
  • Church-Rosser theorem
  • clause selection
  • colors
  • commands, Emacs
  • commands, server
  • Config.append
  • Config.load
  • Config.read
  • Configurations
  • constraint domains
  • constraints
  • context, regular
  • coverage
  • current declaration
  • cut elimination

    • d

  • decl
  • declaration
  • declaration, current
  • declarations
  • declarations, mode
  • declarations, name preference
  • declarations, operator
  • declarations, reduction
  • declarations, termination
  • declarations, theorem
  • definitions
  • definitions, family-level
  • definitions, in proof search
  • definitions, strict
  • definitions, type-level
  • display, of server buffer
  • documentation

    • e

  • editing
  • Emacs variables
  • environment parameters
  • error messages
  • error tracking
  • examples, from user's guide
  • executing proofs
  • existential quantifier

    • f

  • faces
  • family-level definitions
  • file
  • file names
  • files, configuration
  • files, loading
  • filling
  • first-order logic
  • free variables
  • freezing families

    • g

  • get

    • h

  • help
  • Hilbert calculus
  • Horn logic, theory

    • i

  • id
  • identifiers, reserved
  • implicit arguments
  • implicit quantifiers
  • indentation
  • info file
  • initializing Twelf mode
  • input coverage
  • input mode
  • installation
  • interrupt

    • k

  • kinds
  • Kolmogorov translation

    • l

  • lambda calculus example
  • lambda-calculus, polymorphic
  • lambda-calculus, untyped
  • left
  • LF
  • limit
  • load-path
  • loadFile
  • loading files
  • local assumptions
  • local parameters
  • logic programming
  • logic programming, theory
  • logical framework

    • m

  • M-x backward-delete-char-untabify
  • M-x find-tag
  • M-x find-tag-other-window
  • M-x tags-loop-continue
  • M-x tags-query-replace
  • M-x tags-search
  • M-x twelf-check-declaration
  • M-x twelf-font-fontify-buffer
  • M-x twelf-font-fontify-decl
  • M-x twelf-font-unfontify
  • M-x twelf-get
  • M-x twelf-goto-error
  • M-x twelf-indent-decl
  • M-x twelf-indent-line
  • M-x twelf-indent-region
  • M-x twelf-info
  • M-x twelf-mode
  • M-x twelf-next-error
  • M-x twelf-print-program
  • M-x twelf-print-signature
  • M-x twelf-print-subord
  • M-x twelf-print-tex-program
  • M-x twelf-print-tex-signature
  • M-x twelf-reset
  • M-x twelf-save-check-config
  • M-x twelf-save-check-file
  • M-x twelf-server
  • M-x twelf-server-configure
  • M-x twelf-server-display
  • M-x twelf-server-interrupt
  • M-x twelf-server-quit
  • M-x twelf-server-restart
  • M-x twelf-server-send-command
  • M-x twelf-set
  • M-x twelf-sml
  • M-x twelf-sml-cd
  • M-x twelf-sml-quit
  • M-x twelf-sml-send-newline
  • M-x twelf-sml-send-query
  • M-x twelf-sml-send-region
  • M-x twelf-sml-send-semicolon
  • M-x twelf-tag
  • M-x twelf-timers-check
  • M-x twelf-timers-reset
  • M-x twelf-timers-show
  • M-x twelf-to-twelf-sml-mode
  • M-x twelf-trace-break
  • M-x twelf-trace-break-all
  • M-x twelf-trace-show
  • M-x twelf-trace-trace
  • M-x twelf-trace-trace-all
  • M-x twelf-trace-unbreak
  • M-x twelf-trace-untrace
  • M-x twelf-type-const
  • make
  • meta-logic
  • meta-theorem verification, meta-theorem verification
  • Mini-ML, compilation
  • Mini-ML, theory
  • Mini-ML, with units
  • ML implementations
  • ML interface
  • MLton
  • mode checking
  • mode declaration, full form
  • mode declarations, short form
  • modes
  • mutual arguments
  • mutual recursion

    • n

  • name preferences
  • nat
  • natural deduction
  • none
  • numbers

    • o

  • objects
  • occurrences, rigid
  • occurrences, strict
  • open
  • operational semantics
  • operator declarations
  • order
  • order, lexicographic
  • order, simultaneous
  • order, subterm
  • ordered logic
  • OS.chDir
  • OS.exit
  • OS.getDir
  • output coverage
  • output mode

    • p

  • parameter block
  • parameters
  • parameters, environment
  • Poly/ML
  • precedence
  • Print.domains
  • Print.prog, Print.prog
  • Print.sgn, Print.sgn
  • Print.subord
  • printing, from Emacs
  • printing, signature
  • proof realizations

    • q

  • quantifier, existential
  • quantifier, universal
  • quantifiers, implicit
  • queries
  • queries, interactive
  • quit

    • r

  • reconTraceMode
  • recursion
  • reduction declarations
  • reduction predicate
  • regular context, regular context
  • regular worlds
  • reserved characters
  • reserved identifiers
  • reset
  • right
  • rigid occurrences
  • running time

    • s

  • search strategy
  • semantics, operational
  • server
  • server buffer
  • server commands
  • server parameters, setting
  • server state
  • server timers
  • server types
  • set
  • setting server parameters
  • signature
  • signature printing
  • signature TWELF
  • solving queries
  • splitting
  • Standard ML of New Jersey
  • statistics
  • strategy
  • strict definitions
  • strict occurrences
  • structure Twelf
  • subgoal selection
  • subordination
  • subterm order
  • syntax highlighting

    • t

  • Table.top
  • tabled logic programming
  • tableStrategy
  • tagging configurations
  • tags file
  • term
  • term reconstruction
  • termination checking
  • termination declarations
  • termination order
  • TeX output
  • theorem declarations
  • theorem prover
  • Timers.check
  • Timers.reset
  • Timers.show
  • timing statistics
  • top
  • top-level, query
  • totality
  • Trace.break
  • Trace.breakAll
  • Trace.detail
  • Trace.reset
  • Trace.show
  • Trace.trace
  • Trace.traceAll
  • Trace.unbreak
  • Trace.untrace
  • tracing reconstruction
  • tracing, from Emacs
  • tracking errors
  • Twelf home page
  • Twelf mode in Emacs
  • Twelf server
  • twelf-indent
  • twelf-info-file
  • twelf-mode-hook
  • twelf-server-mode-hook
  • twelf-server-program
  • Twelf-SML mode
  • twelf-sml-mode-hook
  • twelf-sml-program
  • Twelf.ABORT
  • Twelf.chatter
  • Twelf.Compile.optimize, Twelf.Compile.optimize
  • Twelf.Config.append
  • Twelf.Config.define
  • Twelf.Config.load
  • Twelf.Config.read
  • Twelf.Config.suffix
  • Twelf.doubleCheck
  • Twelf.loadFile
  • Twelf.make
  • Twelf.OK
  • Twelf.OS.chDir
  • Twelf.OS.getDir
  • Twelf.Print.depth
  • Twelf.Print.implicit, Twelf.Print.implicit
  • Twelf.Print.indent
  • Twelf.Print.length
  • Twelf.Print.prog
  • Twelf.Print.sgn
  • Twelf.Print.subord
  • Twelf.Print.TeX.prog
  • Twelf.Print.TeX.sgn
  • Twelf.Print.width
  • Twelf.Prover.FRS
  • Twelf.Prover.maxRecurse, Twelf.Prover.maxRecurse
  • Twelf.Prover.maxSplit, Twelf.Prover.maxSplit
  • Twelf.Prover.RFS
  • Twelf.Prover.strategy, Twelf.Prover.strategy
  • Twelf.Recon.Omiscient
  • Twelf.Recon.Progressive
  • Twelf.Recon.trace
  • Twelf.Recon.TraceMode
  • Twelf.Recon.traceMode
  • Twelf.reset
  • Twelf.Table.strategy, Twelf.Table.strategy
  • Twelf.Table.strengthen, Twelf.Table.strengthen
  • Twelf.Table.Subsumption
  • Twelf.Table.top
  • Twelf.Table.Variant
  • Twelf.Timers.check
  • Twelf.Timers.reset
  • Twelf.Timers.show
  • Twelf.Trace.All
  • Twelf.Trace.break
  • Twelf.Trace.detail
  • Twelf.Trace.None
  • Twelf.Trace.reset
  • Twelf.Trace.show
  • Twelf.Trace.Some
  • Twelf.Trace.trace
  • Twelf.unsafe, Twelf.unsafe
  • type ascription
  • type checking, from Emacs
  • type families
  • type inference example
  • type reconstruction
  • type-level definitions
  • types
  • types, server
  • typographical conventions

    • u

  • unification
  • universal quantifier

    • v

  • variable naming
  • variable scope
  • variables, bound
  • variables, Emacs
  • variables, free

    • w

  • world checking

    • Go to the first, previous, next, last section, table of contents.