Zulip Chat Archive

Stream: new members

Topic: attribute [intro]


view this post on Zulip Kenny Lau (Oct 19 2018 at 00:01):

What does this attribute do? I saw it here:

inductive Exists {α : Sort u} (p : α  Prop) : Prop
| intro (w : α) (h : p w) : Exists

attribute [intro] Exists.intro

and when I hover it says "introduction rule for backward chaining"


Last updated: May 11 2021 at 22:14 UTC