beluga.vim/syntax/beluga.vim

if exists('b:current_syntax')
  finish
endif
let b:current_syntax = 'beluga'

setlocal iskeyword=@,48-57,63-64,a-z,A-Z,!,$,&,',*,+,_,/,=,-,~,#,^
setlocal comments=b:%,srn:%{,m:\ ,ern:}%
setlocal commentstring=%%s

syn match belArrowEtc /->\|=>\|→\|⇒\||-#\?\|⊢\|\<=\>\|:/
hi def link belArrowEtc Function

syn match belDelim /[()\]{}.;,]\|[#$]\?\[\|\<\/\>\||-\@!\|<\|-\@<!>/
hi def link belDelim Delimiter

syn match belComment /%.*$/
hi def link belComment Comment

syn region belBlockComment start='%{' end='}%' contains=belBlockComment
hi def link belBlockComment belComment

syn keyword belUnderscore _ #_ $_
hi def link belUnderscore Special

syn keyword belType type ctype
hi def link belType Typedef

syn match belPragma /\%(%\|\<--\)\%(coverage\|warncoverage\|nostrengthen\|infix\|prefix\|assoc\|name\|abbrev\|not\|open\)\>/
hi def link belPragma Special

syn keyword belDecl
  \ LF inductive coinductive stratified proof schema rec and typedef
hi def link belDecl Structure

syn keyword belTotal total
hi def link belTotal Special

syn keyword belTrust trust
hi def link belTrust Underlined

syn keyword belSubstConst ^
syn match belSubstConst /\.\./
hi def link belSubstConst Constant

syn keyword belIdBlock some block
hi def link belIdBlock Structure

syn keyword belModule module struct end
hi def link belModule Structure

syn match belQualName /\>::\</
hi def link belQualName Normal

syn match belVarVar /#\k\+/
hi def link belVarVar Constant

syn match belSubstVar /\$\k\+/
hi def link belSubstVar String

syn region belObjLam
  \ matchgroup=belObjLamP start=/\\/ matchgroup=belArrowEtc end=/\./ transparent
hi def link belObjLamP Function

syn keyword belMetaLam fn mlam fun
hi def link belMetaLam Define

syn keyword belCase case of impossible
hi def link belCase Keyword

syn keyword belLet let in
hi def link belLet Keyword

syn match belSubBlock /\.\k\+\>/
hi def link belSubBlock Label

" bools are gone
" but if/then/else are still keywords that don't do anything ☹

" syn keyword belBoolType Bool
" hi def link belBoolType Typedef

" syn keyword belBool ttrue ffalse
" hi def link belBool Boolean

syn keyword belIf if then else
hi def link belIf Error

syn match belugaError /<-\|←/
syn keyword belugaError prop
hi def link belugaError Error

syn match belugaHole /\<?\k*\>/
hi def link belugaHole Underlined