The doc parser doesn't seem to always capture references, but rather introduces new shadowing bindings

[mitchellwrosen]

> {{ ``Nat.and (Nat.or 1 2)`` }}

Expected output:

Paragraph [ Special (Example 1 (Term.Term (Any (do Nat.and (Nat.or 3 4))))) ]

Actual output:

Paragraph [ Special (Example 1 (Term.Term (Any (do Nat.or -> Nat.and (Nat.or 3 4))))) ]

For some reason Nat.or is introduced as a variable, rather than resolved to the Nat.or in the environment.

[pchiusano]

This is (for better or worse) as designed. The syntax doesn't know what the user intends to be a free variable that's a wildcard in the example and what the user intends to be bound, and the decision needs to be made at parse time when that portion of the AST is created. The reason is that examples with variables as in List.map f [1,2,3] are represented in the doc AST with a lambda like (f -> List.map f [1,2,3]).

Right now the parser uses the following logic: the head of the expression is resolved, and all other symbols are left as free variables. It's optimized for the common case of examples like List.map f xs. Or List.map f [1,2,3].

You can use the syntax {{ docExample 0 do Nat.and (Nat.or 1 2) }}. The 0 controls how many of the free variables are elided from the rendering of the lambda.

{{ docExample 2 do (x y -> x Nat.+ y) }} will render as x Nat.+ y, eliding the lambda that introduces those variables.

An idea I had to improve this is to never treat multi-segment names as free variables. So if you write Nat.or within the double backticks then tries to treat that as a function reference (and fails with a name resolution error if it can't resolve).

Another possibility is don't have any special syntax for variables in these inline examples, and force people to use the explicit transclusion syntax for those. Maybe that could get better syntax sugar (like the variables have a $ in front of them or something).