racket / racket/redex

documentation: what are generation failures

Open
#201 4 comments 0 reactions 1 assignee View on GitHub

@wilbowma is already working on this.

Since Oct 4, 2019.

Dominant language
Racket
Stars
112
Forks
42
PR merge metrics
No merged PRs in 30d

Description

I have a program using redex-check that looks like


> (redex-check
    BoxyTypingL
    #:satisfying (type-infer · · e A)
    (redex-match? BoxyEvalL v (term (eval e)))
    #:attempts 1000)
redex-check: no counterexamples in 78 attempts (with 922 generation failures)

I cannot for the life of me figure out why there would be so many failures, and looking through the documentation, I don't see any references that help me make sense of it.

As I understand #:satsifying, there ought not be any failures! It should have generated a bunch of well-typed terms...

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.