Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
Java
Bitcoin
Ethereum
Yul
C
Atc
Syntax-for-tools
Abstract-syntax
Expr
Exprs/decls
Binop
Abstract-syntax-operations
Tyspec
Amb-expr/tyname
Dirdeclor
Stmt
Unop
Dec/oct/hex-const
Simple-escape
Dirabsdeclor
Ident
Amb-declor/absdeclor
Paramdeclor
Transunit-ensemble
Stoclaspec
Declor
Alignspec
Lsuffix
Declspec
Hex-frac-const
Dec-frac-const
Dec-core-fconst
Strunispec
Structdecl
Expr-option
Dirabsdeclor-option
Desiniter
Absdeclor
Tyqual
Isuffix
Amb?-declor/absdeclor
Hex-core-fconst
Escape
Structdeclor
Specqual
Label
Const-expr-option
Bin-expo
Amb?-expr/tyname
Fundef
Fsuffix
Enumspec
Absdeclor-option
Tyname
Stringlit
Paramdecl
Initer-option
Declor-option
Const
Oct-escape
Oct-escape-fix
Oct-escape-case
Oct-escape-equiv
Oct-escapep
Oct-escape-three
Oct-escape-three->digit3
Oct-escape-three->digit2
Oct-escape-three->digit1
Make-oct-escape-three
Change-oct-escape-three
Oct-escape-two
Oct-escape-one
Oct-escape-kind
Initer
Iconst
Hex-quad
Eprefix
Dec-expo
Cprefix-option
Const-expr
S-char
Isuffix-option
Ident-option
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Sign-option
Inc/dec-op
Iconst-option
Genassoc
Decl
Const-option
Usuffix
Univ-char-name
Statassert
Designor
Sign
Hprefix
Block-item
Initdeclor
Funspec
Enumer
Dec-expo-prefix
Bin-expo-prefix
Extdecl
Cconst
Transunit
Inc/dec-op-list
Declspec-list
Tyqual-list
Specqual-list
S-char-list
Decl-list
C-char-list
Structdeclor-list
Structdecl-list
Paramdecl-list
Initdeclor-list
Genassoc-list
Extdecl-list
Desiniter-list
Stmts/blocks
File-paths
Enumer-list
Block-item-list
Tyqual-list-list
Filepath-transunit-map
Stoclaspec-list
Ident-list
Expr-list
Designor-list
Tyspec-list
Parser
Printer
Mapping-to-language-definition
Read-files
Print-files
Read-and-parse-files
Parse-files
Concrete-syntax
Write-files
Print-and-write-files
Preprocessing
Language
Representation
Pack
Transformation-tools
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Oct-escape
Oct-escape-three
This is a product type, introduced by
fty::deftagsum
in support of
oct-escape
.
Fields
digit1 —
oct-digit-char
digit2 —
oct-digit-char
digit3 —
oct-digit-char
Subtopics
Oct-escape-three->digit3
Get the
digit3
field from a
oct-escape-three
.
Oct-escape-three->digit2
Get the
digit2
field from a
oct-escape-three
.
Oct-escape-three->digit1
Get the
digit1
field from a
oct-escape-three
.
Make-oct-escape-three
Basic constructor macro for
oct-escape-three
structures.
Change-oct-escape-three
Modifying constructor for
oct-escape-three
structures.