.textidote

-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

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

replacements.txt

# 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

textidote-flycheck.el

(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))
  )