Jacob Salzberg (Oct 28 2022 at 23:30): 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.
They did say earlier that [] lists type judgements, but even if so I'm not sure I understand what they're then saying here.
Jacob Salzberg (Oct 28 2022 at 23:37):oopsadaisy, this is super easy, they're just giving the derivation tree for ex.
Notification Bot (Oct 28 2022 at 23:37):Jacob Salzberg has marked this topic as resolved.
Pierre Castéran (Oct 29 2022 at 06:56):Looks like the brackets are a typo. Sorry!
Last updated: Oct 04 2023 at 20:01 UTC