Users who actually try the examples in VS Code will be confused when a comment disagrees with what they see when they hover. I think the first such example is
#check Nat.add -- Nat → Nat → Nat
A user reading the tutorial will be completely befuddled by the crosses and the superscript. The main problem is that this undermines reader trust, either in the tool or in the comments. (Note that this is different from leaving something unexplained; here you are saying that they will see one thing, and they actually see another.) You can avoid this by just having an explanation, a forward pointer, or some sort of warning in the comment, the hover, or in the text.
There are also examples where the comment should just be changed to match the hover, as in
#check ident -- ?m → ?m
Users who actually try the examples in VS Code will be confused when a comment disagrees with what they see when they hover. I think the first such example is
#check Nat.add -- Nat → Nat → NatA user reading the tutorial will be completely befuddled by the crosses and the superscript. The main problem is that this undermines reader trust, either in the tool or in the comments. (Note that this is different from leaving something unexplained; here you are saying that they will see one thing, and they actually see another.) You can avoid this by just having an explanation, a forward pointer, or some sort of warning in the comment, the hover, or in the text.
There are also examples where the comment should just be changed to match the hover, as in
#check ident -- ?m → ?m