Najkrotsza sesja Coqa.

  Coq < Quit.

  [zawodnik@maszyna]$

  zeby miec historie i edycje linii:
  [zawodnik@maszyna]$ ledit coqtop

  albo w buforze shellowym w emacsie

Termy

• Prop oznacza typ "proposition",
• "identycznosc na typie A" ("\lambda x:A.x") to [x:A]x
• "dla kazdego A i B, A implikuje B" ("\forall A \forall B. A->B"), to (A,B:Prop)A->B

Komendy trybu normalnego

Definition nazwa := term.
Definition nazwa : typ := term.
- wprowadza definicje do srodowiska

Parameter nazwa : typ.
- wprowadza zmienna do srodowiska

Lemma nazwa : formula.
Theorem nazwa : formula.
- przechodzi do trybu wpisywania dowodow, po szczesliwym zakonczeniu wprowadza lemat/twierdzenie do srodowiska

Goal formula.
- j.w. tylko wprowadza nazwe Unnamed_thm, chyba ze zakonczymy dowod przez Save nazwa.

Check term.
- wyswietla typ termu

Print nazwa.
- wyswietla definicje stalej

Reset  nazwa.
-  kasuje wszystkie obiekty wprowadzone do srodowiska po "nazwa" (wlacznie z "nazwa").

Reset Initial.
- kasuje wszystko od poczatku sesji Coqa
 

Tryb dowodowy.

Taktyki

Apply term.

Assumption.

Auto.

Unfold nazwa.
Unfold 1 2 3 nazwa.
Unfold nazwa in H.

Apply H; Intros. <- robi Intros dla kazdego subgoala generowanego przez Apply H.

Komendy

Koniec dowodu

Chodzenie po sub-goalach

Wyswietlanie

Rezygnacja