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 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 /\/ hi def link belugaHole Underlined