Index of concepts for Week 02

• denotation
• equality (Leibniz)
• existential quantifier (exists)
• exists (in the goal)
• forall (in the goal)
• logical conjunction
• logical disjunction
• logical equivalence
• modus ponens
• modus tollens
• naming conventions
• quantifier (existential)
• quantifier (universal)
• universal quantifier (forall)
• tCPA constructor (conj)
• tCPA keyword (Abort)
• tCPA keyword (Admitted)
• tCPA keyword (admit)
• tCPA keyword (Proof)
• tCPA keyword (Qed)
• tCPA command (Search)
• tCPA tactic (apply)
• tCPA tactic (destruct)
• tCPA tactic (exact)
• tCPA tactic (intro)
• tCPA tactic (intros)
• tCPA tactic (reflexivity)
• tCPA tactic (revert)
• tCPA tactic (rewrite)
• tCPA tactic (split)
• tCPA tactic (symmetry)
• tCPA tactic (unfold)

Version

Added the entry about Leibniz equality [15 Apr 2024]

Created [25 Jan 2024]