Skip to content

citp goal

Norbert Preining edited this page Oct 6, 2017 · 2 revisions

:goal { <sentence> . ... }

Define the initial goal for CITP

Related: citp

Example

CafeOBJ> select PNAT .
PNAT> :goal { 
   eq [lemma-1]: M:PNat + 0 = M . 
   eq [lemma-2]: M:PNat + s N:PNat = s( M + N ) . 
}
Clone this wiki locally