Skip to main content

Questions tagged [refinement-type]

Refinement types are types annotated with predicates.

Filter by
Sorted by
Tagged with
9 votes
2 answers
373 views

What's the relationship between refinement types and dependent types?

In the F* proof assistant, they use refinement types together with dependent types. Based on my impression of F*, it seems to me that refinement types are just predicates in dependent type theory that ...
ice1000's user avatar
  • 6,186