Skip to content

Instantly share code, notes, and snippets.

@JoeyEremondi
Last active June 4, 2022 23:20
Show Gist options
  • Save JoeyEremondi/63ee4891d9691c5dc14f39dfab2c1c2e to your computer and use it in GitHub Desktop.
Save JoeyEremondi/63ee4891d9691c5dc14f39dfab2c1c2e to your computer and use it in GitHub Desktop.
-remove-macros je,rg,et
--remove theorem,theoremEnd,proof,proofEnd,align,align*,flalign,flalign*,array,displaymath
--check en
--output html
--replace replacements.txt
--dict dictionary.txt
equalities
adjunction
metatheory
canonicity
boolean
booleans
ascriptions
codomain
scrutinee
Idris
Agda
coq
extensibility
parameterization
parameterizations
monotonicity
observationally
decidability
upcast
upcasts
minimality
equi-precise
equi-precision
inconvertible
conservativity
convertibility
Definitionally
idempotence
well-behavedness
graduality
X's
Y's
datatype
datatypes
bidirectionality
typability
Girard
embeddings
Agda-like
Peano
compositional
difficulty
untyped
invariants
quicksort
definitional
propositional
inductives
notational
gradualizing
definitionally
propositionally
convertability
grey
metafunction
metavariable
metavariables
expressivity
# Empty lines beginning with a pound sign are ignored
# Search and replace patterns are separated by a tab
\\lang\S Y
\\clang\S Y
\\celang\S Y
\\cilang\S Y
\\tlang\S Y
\\surflang\S X
\\surfelang\S X
\\surfilang\S X
\\slang\S X
\\lang\s Y
\\clang\s Y
\\celang\s Y
\\cilang\s Y
\\surflang\s X
\\surfelang\s X
\\surfilang\s X
\\slang\s X
\\tlang\s Y
\\MLTT type-theory
\\ie i.e.
\\eg e.g.
\\rrule\{.*\}\s X
\\rrule\{.*\}\S X
\\je\{.*\} \
\\citet\{.*\} authors
\\Citet\{.*\} Authors
GCIC X
GDTL X
\ iff \ if
# Patterns can also be regular expressions
(setq flycheck-check-syntax-automatically '(mode-enabled save))
(flycheck-define-checker textidote
"Check LaTeX spelling and grammar"
:command ("textidote" "--output" "singleline" "--no-color" "--read-all" "--ci" source)
:error-patterns
((error line-start (file-name) "(L" line "C" column "-L" end-line "C" end-column "):" (message) line-end))
:modes latex-mode
;; :next-checkers ((warning . lsp))
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment