From dd083c69d639009bbc54bc45730bb5edaaa7fbf2 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Wed, 18 Oct 2023 14:10:11 -0400 Subject: [PATCH] notes for expanding practices --- templates/teaching/practices.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/templates/teaching/practices.md b/templates/teaching/practices.md index 5709b24334..e83276b147 100644 --- a/templates/teaching/practices.md +++ b/templates/teaching/practices.md @@ -24,7 +24,11 @@ and can help you choose materials to use. Have they programmed in a functional language, or in any language? Can they be expected to install Lean locally on their own computer? -* +* [warning about not introducing too many tactic variants] + +* [discussing type theory vs set theory] + +* [how much Lean to use -- essential or incidental? Do students use it mandatory, optional, just you?] ## Organizing course projects @@ -39,6 +43,7 @@ Without some kind of structure like this -- for example, if students receive bar it is hard to ensure that they all use the same version of Lean. It is also a good way to provide a "library" file or files containing basic definitions, tactics, and such that are useful for your course. +[if you are distributing bare Lean files...] These projects are often hosted on GitHub. Students are asked to clone the project, or create a Codespace or Gitpod instance,