describe fields and tags in yaml file

data/courses.yaml

@@ -1,3 +1,21 @@
+# Entries in this file should have the following fields:
+# 
+# `name`: the title of the course
+# `instructor`: the name of the person or people who taught the course
+# `year`: the most recent year the course was taught
+# `summary`: a description of what was covered and done in the course
+# `tags`: a list of tags (see below)
+# `website` (optional): the course's home page
+# `material` (optional): a link to a textbook, course notes, etc
+# `repository` (optional): a link to the course's project repository, e.g. on GitHub
+# `experiences` (optional): a reflection about how the course went, things that could be done differently, etc
+# `language` (optional): if the instruction language was not English, what language was it?
+#
+# Please use tags that are shown on the website. In particular, each entry should have
+# a Lean version tag (`lean3` or `lean4`) and a general subject 
+# (`mathematics`, `logic`, `computer science`). 
+# 
+
 - name: Some high-school mathematics in Lean
   instructor: Peter Pfaffelhuber
   location: University of Freiburg, Germany
@@ -219,15 +237,16 @@
   instructor: Robert Y. Lewis
   location: Brown University
   website: https://browncs1951x.github.io/
-  material: https://github.com/BrownCS1951x/fpv2022
-  tags: ['formalization of mathematics', 'logic', 'verification', 'lean3']
+  material: https://lean-forward.github.io/hitchhikers-guide/2023/
+  repository: https://github.com/BrownCS1951x/fpv2023
+  tags: ['formalization of mathematics', 'logic', 'verification', 'lean4']
   summary: >
     This is an upper level undergraduate/graduate course that teaches the theory and practice of proof assistants using Lean.
     Topics covered include verification of functional programs, PL semantics, mathematical structures, metaprogramming,
     and logical foundations. The course is based on Jasmin Blanchette's course Logical Verification and uses the
     Hitchhiker's Guide to Logical Verification as a reference.
   experiences: >
-    I have taught this course twice at Brown and it has proven to be quite popular, attracting a mixed audience
+    I have taught this course three times at Brown and it has proven to be quite popular, attracting a mixed audience
     of people interested in math/logic, PL research, and functional programming. Final projects have included a verified
     executable DPLL SAT solver; the mathlib tactic `linear_combination` and initial work toward `polyrith` explorations
     of axiomatic ZFC, linear algebra, and other mathematical topics; and more.
@@ -236,7 +255,7 @@
   instructor: Robert Y. Lewis
   location: Brown University
   website: https://cs22.io/
-  material: https://github.com/brown-cs22/CS22-Lean-2023
+  repository: https://github.com/brown-cs22/CS22-Lean-2023
   tags: ['intro to proofs', 'number theory', 'combinatorics', 'lean4']
   summary: >
     This is a large introductory course that is taken by most computer science students at Brown.