Stream: Coq users

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Audrey Seo (Jan 29 2023 at 01:10):

Oh, that would make sense! Thanks!

Last updated: Jun 25 2024 at 15:02 UTC