document the variable attr

Author: nikomatsakis

book/src/formality_core/terms.md

@@ -35,7 +35,8 @@ The `#[term]` macro says that these are terms and we should generate all the boi
 
 The `#[term]` also accepts some internal annotations:
 
-* `#[cast]` can be applied on an enum variant with a single argument. It says that we should generate upcast/downcast impls to allow conversion. In this case, between a `Variable` and an `Expr`. This would generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+* `#[cast]` can be applied on an enum variant with a single argument. It says that this variant represents an "is-a" relationship and hence we should generate upcast/downcast impls to allow conversion. In this case, a variable is a kind of expression -- i.e,. wrapping a variable up into an expression doesn't carry any semantic meaning -- so we want variables to be upcastable to expressions (and expressions to be downcast to variables). The `#[cast]` attribute will therefore generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+    * There is a special case version of `#[cast]` called `#[variable]`. It indicates that the variant represents a (type) variable -- we are not using it here because this an expression variable. Variables are rather specially in folding/parsing to allow for substitution, binders, etc.
 * `#[grammar]` tells the parser and pretty printer how to parse this variant. The `$v0` and `$v1` mean "recursively parse the first and second arguments". This will parse a `Box<Expr>`, which of course is implemented to just parse an `Expr`.
 
 If you are annotating a struct, the `#[term]` just accepts the grammar directly, so `#[term($name)] struct Variable`  means "to parse a variable, just parse the name field (a string)".