The Rocq Standard Library
9.0
  • Introduction and Contents

Overview

  • The standard library
    • Survey
    • Peano’s arithmetic (nat)
    • Notations for integer arithmetic
    • Real numbers library
      • Notations for real numbers
      • Some tactics for real numbers
    • List library
    • Floats library
    • Primitive strings library

Appendix

  • Recent changes
    • Previous versions
  • Bibliography
The Rocq Standard Library
  • »
  • Index
  • Edit on GitHub

Index

Symbols | A | D | F | H | L | M | N | P | R | S | T

Symbols

  • * (term)
  • + (term)
  • - (term)
  • < (term)
  • <= (term)
  • > (term)
  • >= (term)
  • ?= (term)

A

  • app (term)
  • Arithmetical notations

D

  • discrR (tactic)

F

  • flat_map (term)
  • fold_left (term)
  • fold_right (term)

H

  • head (term)

L

  • length (term)

M

  • map (term)
  • mod (term)

N

  • nat_scope
  • Notations for lists
  • nth (term)

P

  • Peano's arithmetic
  • Printing Float (flag)

R

  • rev (term)

S

  • singel: / (term)
  • split_Rabs (tactic)
  • split_Rmult (tactic)

T

  • tail (term)
  • The constant number is not a binary64 floating-point value. A closest value number will be used and unambiguously printed number. [inexact-float,parsing] (warning)

© Copyright 1999-2024, Inria, CNRS and contributors.

Built with Sphinx using a theme provided by Read the Docs.
Other versions v: 9.0
Versions
dev
stable
9.0
8.20
8.19
8.18
8.17
8.16
8.15
8.14
8.13
8.12
8.11
8.10
8.9
8.8
8.7
8.6
8.5
8.4
8.3
8.2
8.1
8.0
Downloads