Coq
8.8.2

索引

  • Index
  • Command index
  • Tactic index
  • Flags, options and tables index
  • Errors and warnings index

はじめに

  • はじめに
  • Credits

言語

  • 仕様記述言語 Gallina
  • Gallina の拡張
  • The Coq library
  • Calculus of Inductive Constructions
  • The Module System

証明エンジン

  • Vernacular commands
  • Proof handling
  • Tactics
  • The tactic language
  • Detailed examples of tactics
  • The SSReflect proof language

ユーザ拡張

  • Syntax extensions and interpretation scopes
  • Proof schemes

実用ツール

  • The Coq commands
  • Utilities
  • Coq Integrated Development Environment

付録

  • Extended pattern matching
  • Implicit Coercions
  • 正準構造
  • 型クラス
  • Omega: a solver for quantifier-free problems in Presburger Arithmetic
  • Micromega: tactics for solving arithmetic goals over ordered rings
  • Extraction of programs in OCaml and Haskell
  • Program
  • The ring and field tactic families
  • Nsatz: tactics for proving equalities in integral domains
  • Generalized rewriting
  • Asynchronous and Parallel Proof Processing
  • Miscellaneous extensions
  • Polymorphic Universes

Reference

  • Bibliography
Coq
  • »
  • 検索

© Copyright 1999-2018, Inria.

Built with Sphinx using a theme provided by Read the Docs.