fix constructor name in comment
This commit is contained in:
parent
9ecaaf72bd
commit
69f032584e
1 changed files with 1 additions and 1 deletions
|
@ -19,7 +19,7 @@ import Derive.Prelude
|
||||||
||| @ Reserved reserved token
|
||| @ Reserved reserved token
|
||||||
||| @ Name name, possibly qualified
|
||| @ Name name, possibly qualified
|
||||||
||| @ Nat nat literal
|
||| @ Nat nat literal
|
||||||
||| @ String string literal
|
||| @ Str string literal
|
||||||
||| @ Tag tag literal
|
||| @ Tag tag literal
|
||||||
||| @ TYPE "Type" or "★" with ascii nat directly after
|
||| @ TYPE "Type" or "★" with ascii nat directly after
|
||||||
||| @ Sup superscript or ^ number (displacement, or universe for ★)
|
||| @ Sup superscript or ^ number (displacement, or universe for ★)
|
||||||
|
|
Loading…
Reference in a new issue