search

kosmikus / lhs2tex

Preprocessor for typesetting Haskell sources with LaTeX
Other
99 stars 28 forks source link

The list of keywords in Agda is outdated #91

Closed L-TChen closed 1 year ago

L-TChen commented 1 year ago

The current list of Agda keywords

keywords Agda                 =  [ "let", "in", "where", "field", "with",
                                   "postulate", "primitive", "open", "import",
                                   "module", "data", "codata", "record", "infix",
                                   "infixl", "infixr", "mutual", "abstract",
                                   "private", "forall", "using", "hiding",
                                   "renaming", "public" ]

in https://github.com/kosmikus/lhs2tex/blob/master/src/HsLexer.lhs is outdated.

Some keywords have been added in or before Agda 2.6.3:

coinductive constructor do eta-equality inductive instance interleaved macro no-eta-equality overlap pattern quote quoteTerm rewrite syntax tactic unquote unquoteDecl unquoteDef variable

while the following has been removed:

codata