Work Plan for Week 3

Material

name file name short version note
Logic in Coq Logic[.html|.v] download
Inductively Defined Propositions IndProp[.html|.v] download

Schedule

date time location type
Monday, 15 September 10:45 - 12:45 CEG - Hall D lecture
Tuesday, 16 September 8:45 - 10:45 CEG - Hall D lecture
Thursday, 18 September 13:45 - 15:45 Pulse - Hall 3 & 6 problem session

Problem Session

file exercises
Logic[.html|.v]
  • and_assoc
  • contrapositive
  • de_morgan_not_or
  • (extra) or_distributes_over_and
  • dist_exists_or
  • In_app_iff
  • both logical_connectives (andb_true_iff and orb_true_iff)
IndProp[.html|.v]
  • ev_sum
  • both total_relation (total_relation and rev_invtotal_relation_is_totalolutive)
  • both empty_relation (empty_relation and empty_relation_is_empty)
  • reflect_iff

Additionally, please fill in this feedback form to let us know what you find helpful and what you would like to see improved in the setup of this course!

If you need help, make a request during the problem session in the Queue or reach out on Mattermost.