doc-src/Nitpick/nitpick.tex
changeset 33581 e1e77265fb1d
parent 33579 da0fea4b6e36
child 33731 040852c71779
equal deleted 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.