Skip to content

Incorrect handling of predicates without base types #49

@codyroux

Description

@codyroux

The following predicate

inductive NoBase : Nat → Prop where
| succ : NoBase n → NoBase (n + 1)

derive_generator ∃ n, NoBase n

gives the error:

parenthesize: uncaught backtrack exception

which is quite confusing, especially in the absence of any syntax to point to.

I'm not sure what the right fix is here, ideally, we'd produce a correct (but useless) generator with a warning, but perhaps there's something simpler to implement.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions