Skip to content

Inductive predicates#198

Draft
mariojppereira wants to merge 3 commits intoocaml-gospel:mainfrom
mariojppereira:inductive_predicates
Draft

Inductive predicates#198
mariojppereira wants to merge 3 commits intoocaml-gospel:mainfrom
mariojppereira:inductive_predicates

Conversation

@mariojppereira
Copy link
Copy Markdown
Contributor

@mariojppereira mariojppereira commented May 18, 2022 •
edited
Loading

This patch proposes to extend Gospel with support for inductive predicates.

ToDo list:

  • extend parser
  • extend untyped AST
  • include positive/negative tests
  • extend typed AST
  • implement type-checking inductive predicates (particular focus on positivity-checking)

@mariojppereira
Inductive predicates (ocaml-gospel#197)
dbdc6af 
Extend Gospel with support for inductive predicates (wip)
@mariojppereira
Applying formatter
cce1970
@pascutto pascutto removed request for n-osborne and pascutto May 23, 2022 09:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@mariojppereira