Coq < Quit.
[zawodnik@maszyna]$
zeby miec historie i edycje linii:
[zawodnik@maszyna]$ ledit coqtop
albo w buforze shellowym w emacsie
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
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.