| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/coqdoc/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 525 B |
|
Quelle verbatim.v Sprache: Coq |
|||||||||
|
(**
<< uint32_t shift_right( uint32_t a, uint32_t shift ) { return a >> shift; } >> This line and the following shows << verbatim >> text: << A stand-alone inline verbatim >> << A non-ended inline verbatim to test line location - item 1 - item 2 is <<verbatim>> - item 3 is <<verbatim>> too [[ A coq block : forall n, n = 0 ]] - <<verbatim>> again, and a formula [ True -> False ] - << multiline verbatim >> - last item [[[ Γ ⊢ A ---- Γ ⊢ A ∨ B ]]] << A non-ended block verbatim to test line location *) ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-04-04