- - allows to handle calculus assertions,
- - check mechanically proofs of these assertions,
- - helps to find formal proofs,
- - extracts a certified program from the constructive proof of its
- formal specification,
+ - allows to handle calculus assertions,
+ - check mechanically proofs of these assertions,
+ - helps to find formal proofs,
+ - extracts a certified program from the constructive proof of its
+ formal specification.
+
+%description -l pl
+Coq to narzêdzie pomagaj±ce w udowadnianiu, które:
+- pozwala uporaæ siê z twierdzeniami dotycz±cymi rachunku
+ ró¿niczkowego,
+- mechanicznie sprawdzaæ dowody tych twierdzeñ,
+- pomagaæ w znalezieniu formalnych dowodów,
+- wyci±gaæ program o dowiedzionej poprawno¶ci z konstruktywnego
+ dowodu jego formalnej specyfikacji.