-- This file:
--   http://anggtwu.net/LEAN/propositional1.lean.html
--   http://anggtwu.net/LEAN/propositional1.lean
--          (find-angg "LEAN/propositional1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/propositional1.lean"))

-- (find-tpinlean4page  22 "3. Propositions and Proofs")
-- (find-tpinlean4text  22    "Propositions and Proofs")
-- (find-tpinlean4page  22 "3.1. Propositions as Types")
-- (find-tpinlean4text  22      "Propositions as Types")
-- (find-tpinlean4page  25 "3.2. Working with Propositions as Types")
-- (find-tpinlean4text  25      "Working with Propositions as Types")
-- (find-tpinlean4page  28 "3.3. Propositional Logic")
-- (find-tpinlean4text  28      "Propositional Logic")
-- (find-tpinlean4page  33 "3.4. Introducing Auxiliary Subgoals")
-- (find-tpinlean4text  33      "Introducing Auxiliary Subgoals")
-- (find-tpinlean4page  34 "3.5. Classical Logic")
-- (find-tpinlean4text  34      "Classical Logic")
-- (find-tpinlean4page  35 "3.6. Examples of Propositional Validities")
-- (find-tpinlean4text  35      "Examples of Propositional Validities")
-- (find-tpinlean4file "propositions_and_proofs.md")
-- (find-tpinlean4file "propositions_and_proofs.md" "Propositions as Types")
-- (find-tpinlean4file "propositions_and_proofs.md" "``(fun x => t) s`` and ``t[s/x]``")
-- (find-tpinlean4file "propositions_and_proofs.md" "``theorem`` command is really a version of")
-- (find-tpinlean4file "propositions_and_proofs.md" "to the left of the colon")
-- (find-tpinlean4file "propositions_and_proofs.md" "\nPropositional Logic\n")


variable (p q : Prop)

example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

#check fun (hp : p) (hq : q) => And.intro hp hq


variable (p q : Prop)

#check p → q → p ∧ q
#check ¬p → p ↔ False
#check p ∨ q → q ∨ p


-- (find-tpinlean4file "propositions_and_proofs.md" "### Conjunction")

variable (p q : Prop)

example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

#check fun (hp : p) (hq : q) => And.intro hp hq



-- Local Variables:
-- coding:  utf-8-unix
-- End: