Coq Notes [DRAFT]
Created at 2016-05-18T01:52:28.000Z

Type of Things

Basic Commands

Reference:

SearchAbout



SearchPattern (_ + _ = _)
=> 

Locate "<->".
=> 
  Notation            Scope     
  "A <-> B" := iff A B : type_scope
                        (default interpretation)
  • Term

  • SearchPattern

  • -

Basic Tactics

ProofGeneral

Installation: http://wp.hiogawa.net/2016/05/08/coq-installation/

  • Commands:

C-c C-n 1ステップ評価 C-c C-u 1step back C-c C-Enter カーソル位置まで評価 C-c C-a C-o SearchPattern C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-n Notation C-c C-a C-l Locate constant (defined ident) (* type check, term reduction ) ( Check combK (S O). ) ( Eval compute in combK (S O). ) ( Locale "::" *) some information about various "search" command in coq. http://d.hatena.ne.jp/airobo/20120708/1341742780