Stream: Coq users

Topic: ✔ Notation In Coq'Art


view this post on Zulip Jacob Salzberg (Oct 28 2022 at 23:30):

Hi All, does anybody know what they're doing with this bracket notation here in Coq'Art? Theyre saying this series of judgements describes existentials.

AskGuys.png

They did say earlier that [] lists type judgements, but even if so I'm not sure I understand what they're then saying here.

view this post on Zulip Jacob Salzberg (Oct 28 2022 at 23:37):

oopsadaisy, this is super easy, they're just giving the derivation tree for ex.

view this post on Zulip Notification Bot (Oct 28 2022 at 23:37):

Jacob Salzberg has marked this topic as resolved.

view this post on Zulip Pierre Castéran (Oct 29 2022 at 06:56):

Looks like the brackets are a typo. Sorry!


Last updated: Feb 01 2023 at 12:30 UTC