• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
          • Process-syntheto-toplevel-fn
          • Translation
          • Language
            • Static-semantics
            • Abstract-syntax
              • Expression
              • Expression-sum-field-list
              • Type
              • Binary-op
              • Expression-product-field-list
              • Abstract-syntax-operations
              • Function-definition-list->header-list
              • Type-definition-list->name-list
              • Initializer-list->value-list
              • Function-header-list->name-list
              • Typed-variable-list->type-list
              • Typed-variable-list->name-list
              • Branch-list->condition-list
              • Alternative-list->name-list
              • Function-specifier
              • Expression-variable-list
              • Type-subset
              • Field-list->type-list
              • Field-list->name-list
              • Function-specification
              • Identifier
              • Toplevel
              • Function-definer
              • Function-header
              • Type-definer
              • Literal
                • Literal-case
                • Literal-fix
                • Literal-equiv
                • Literalp
                • Literal-string
                • Literal-integer
                • Literal-character
                • Literal-boolean
                • Literal-kind
              • Type-product
              • Function-definition
              • Type-sum
              • Maybe-expression
              • Transform-argument-value
              • Transform
              • Theorem
              • Quantifier
              • Maybe-function-specification
              • Maybe-typed-variable
              • Maybe-type-definition
              • Maybe-function-header
              • Maybe-function-definition
              • Maybe-type-sum
              • Maybe-type-subset
              • Maybe-type-product
              • Maybe-type-definer
              • Maybe-theorem
              • Maybe-type
              • Initializer
              • Type-definition
              • Alternative
              • Unary-op
              • Typed-variable
              • Branch
              • Field
              • Transform-argument
              • Type-recursion
              • Program
              • Function-recursion
              • Typed-variable-list
              • Toplevel-name
              • Toplevel-list
              • Initializer-list
              • Expression-fixtypes
              • Toplevel-fn-names
              • Lookup-transform-argument
              • Function-definition-names
              • Type-definition-list
              • Transform-argument-list
              • Function-header-list
              • Function-definition-list
              • Alternative-list
              • Type-list
              • Identifier-set
              • Identifier-list
              • Field-list
              • Expression-list
              • Branch-list
              • Extract-default-param-alist
              • Create-arg-defaults-table
            • Outcome
            • Abstract-syntax-operations
            • Outcome-list
            • Outcomes
          • Process-syntheto-toplevel
          • Shallow-embedding
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Abstract-syntax

Literal

Fixtype of Syntheto literals.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:boolean → literal-boolean
:character → literal-character
:string → literal-string
:integer → literal-integer

There are literals for all the primitive types.

We plan to restrict the characters usable in character and string literals and also to add certain escapes.

Note that integer literals are non-negative, for simplicity. One can use unary minus to negate an integer literal.

Subtopics

Literal-case
Case macro for the different kinds of literal structures.
Literal-fix
Fixing function for literal structures.
Literal-equiv
Basic equivalence relation for literal structures.
Literalp
Recognizer for literal structures.
Literal-string
Literal-integer
Literal-character
Literal-boolean
Literal-kind
Get the kind (tag) of a literal structure.