Skip to content

Some proofs are failing in the standard library. #212

@kape1395

Description

@kape1395

For example, these are failing in library/SequenceTheorems_proofs.tla:

  • ConcatSimplifications
  • SubSeqProperties
  • SubSeqEmpty
  • HeadTailAppend
  • SequenceEmptyOrAppend

Unsure when the regression happened.
These proofs should probably be checked as part of the test suite.

Metadata

Metadata

Assignees

No one assigned

    Labels

    testingRelated to tests of code, continuous integration, and related topics.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions