diff options
| author | Marshall Lochbaum <mwlochbaum@gmail.com> | 2020-06-27 09:34:47 -0400 |
|---|---|---|
| committer | Marshall Lochbaum <mwlochbaum@gmail.com> | 2020-06-27 09:34:47 -0400 |
| commit | e9f8372e7c6d9efd6c49bfdedf2676a6e11b0ab6 (patch) | |
| tree | 4621a78a5553abb38c1aeea5e637ba571b852ce1 | |
| parent | 246e58abcfc50b6ad7c01ba3d1243128e7ffd4f7 (diff) | |
G isn't a term
| -rw-r--r-- | spec/grammar.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spec/grammar.md b/spec/grammar.md index a2cddf87..ea3aabf5 100644 --- a/spec/grammar.md +++ b/spec/grammar.md @@ -66,7 +66,7 @@ A header looks like a name for the thing being headed, or its application to inp headW = value | "𝕨" headX = value | "𝕩" HeadF = F | "𝕗" | "𝔽" - HeadG = G | "𝕘" | "𝔾" + HeadG = F | "𝕘" | "𝔾" ModH1 = HeadF ( _m | "_𝕣" ) CmpH1 = HeadF ( _c_ | "_𝕣_" ) HeadG valHead = v |