doc-src/Nitpick/nitpick.tex
 changeset 33581 e1e77265fb1d parent 33579 da0fea4b6e36 child 33731 040852c71779
equal inserted replaced
33580:45c33e97cb86 33581:e1e77265fb1d
  2418 \prew
  2418 \prew
  2419 $\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~  2419$\textbf{setup}~\,\{{*}\,~\textit{Nitpick.unregister\_codatatype}~@\{\antiq{typ}~
  2420 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$  2420 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
  2421 \postw
  2421 \postw
  2422
  2422

  2423 Inductive datatypes can be registered as coinductive datatypes, given

  2424 appropriate coinductive constructors. However, doing so precludes

  2425 the use of the inductive constructors---Nitpick will generate an error if they

  2426 are needed.

  2427
  2423 \section{Known Bugs and Limitations}
  2428 \section{Known Bugs and Limitations}
  2424 \label{known-bugs-and-limitations}
  2429 \label{known-bugs-and-limitations}
  2425
  2430
  2426 Here are the known bugs and limitations in Nitpick at the time of writing:
  2431 Here are the known bugs and limitations in Nitpick at the time of writing:
  2427
  2432
  2458
  2463
  2459 \item[$\bullet$] The \textit{nitpick\_} attributes and the
  2464 \item[$\bullet$] The \textit{nitpick\_} attributes and the
  2460 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
  2465 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
  2461
  2466
  2462 \item[$\bullet$] Although this has never been observed, arbitrary theorem
  2467 \item[$\bullet$] Although this has never been observed, arbitrary theorem
  2463 morphisms could possibly confuse Nitpick and lead it to generate spurious
  2468 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
  2464 counterexamples.

  2465
  2469
  2466 \item[$\bullet$] Local definitions are not supported and result in an error.
  2470 \item[$\bullet$] Local definitions are not supported and result in an error.
  2467
  2471
  2468 \item[$\bullet$] All constants and types whose names start with
  2472 \item[$\bullet$] All constants and types whose names start with
  2469 \textit{Nitpick}{.} are reserved for internal use.
  2473 \textit{Nitpick}{.} are reserved for internal use.