Stream: Coq users

Topic: What does this production in the binder grammar mean?

Audrey Seo (Jan 28 2023 at 23:18):

Hello! I was looking through the coq documentation on binders, and I've never seen a binder of the form (name:type|term) but it's listed as one of the productions for binder. Does anyone know what this does? I tried to use it, but it seems to want some kind of prop?

Laurent Théry (Jan 29 2023 at 00:17):

I think it is a way to introduce a function that takes a sig type as argument

Check (fun (x : nat | x < 1) => true).

Audrey Seo (Jan 29 2023 at 01:10):

Oh, that would make sense! Thanks!

Last updated: Oct 04 2023 at 23:01 UTC