aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spec/grammar.md2
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