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?
I think it is a way to introduce a function that takes a
sig type as argument
Check (fun (x : nat | x < 1) => true).
Oh, that would make sense! Thanks!
Last updated: Oct 04 2023 at 23:01 UTC