diff options
| author | Marshall Lochbaum <mwlochbaum@gmail.com> | 2020-06-26 14:38:33 -0400 |
|---|---|---|
| committer | Marshall Lochbaum <mwlochbaum@gmail.com> | 2020-06-26 14:38:33 -0400 |
| commit | c2c2565305d723269ebb28e0c2105bb0712dfeee (patch) | |
| tree | b19c5c279e34cbddb9c26957bcad341d2ec5660f | |
| parent | bfa0be0bbc67047e2ec3f3d457bffdc372e0bcf9 (diff) | |
No ℝ
| -rw-r--r-- | spec/grammar.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/spec/grammar.md b/spec/grammar.md index acb6fb33..691b8c56 100644 --- a/spec/grammar.md +++ b/spec/grammar.md @@ -66,8 +66,8 @@ A header looks like a name for the thing being headed, or its application to inp headX = value | "𝕩" HeadF = F | "𝕗" | "𝔽" HeadG = G | "𝕘" | "𝔾" - ModH1 = HeadF ( _m | "_𝕣" | "_ℝ" ) - CmpH1 = HeadF ( _c_ | "_𝕣_" | "_ℝ_" ) HeadG + ModH1 = HeadF ( _m | "_𝕣" ) + CmpH1 = HeadF ( _c_ | "_𝕣_" ) HeadG valHead = v FuncHead = F | ( headW? ( F | "𝕊" ) )? headX _modHead = _m | ModH1 | headW? ModH1 headX |