git.iko.soy/Idris-dev
on master help sign in
Merge pull request #83 from raichoo/master
eea2d4aEdwin Brady
contribs/tool-support/vim/syntax/idris.vim+2−2
compare with master
unifiedsplit
@@ -10,7 +10,7 @@ syn match idrisModule "\<\(module\|namespace\)\>"
10syn match idrisImport "\<import\>"
10syn match idrisImport "\<import\>"
11syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\)\>"
11syn match idrisStructure "\<\(class\|\(co\)\?data\|instance\|where\|record\)\>"
12syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
12syn match idrisVisibility "\<\(public\|abstract\|private\)\>"
13−syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\|total\|dsl\|auto\|using\|parameters\|mutual\)\>"
13+syn match idrisStatement "\<\(do\|case\|of\|let\|in\|with\|total\|partial\|dsl\|auto\|using\|parameters\|mutual\)\>"
14syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
14syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax"
15syn match idrisConditional "\<\(if\|then\|else\)\>"
15syn match idrisConditional "\<\(if\|then\|else\)\>"
16syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\)\>"
16syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\)\>"
@@ -23,7 +23,7 @@ syn match idrisType "\<\([A-Z][a-zA-Z0-9_]*\|_|_\)\>"
23syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$"
23syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$"
24syn match idrisMetaVar "?[a-z][A-Za-z0-9_]\+"
24syn match idrisMetaVar "?[a-z][A-Za-z0-9_]\+"
25syn match idrisLink "%\(lib\|link\|include\)"
25syn match idrisLink "%\(lib\|link\|include\)"
26−syn match idrisDirective "%\(access\|default\)"
26+syn match idrisDirective "%\(access\|default\|assert_total\)"
27syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+
27syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+
28syn region idrisBlockComment start="{-" end="-}"
28syn region idrisBlockComment start="{-" end="-}"
29syn region idrisProofBlock start="\(default\s\+\)\?proof *{" end="}" contains=idrisTactic
29syn region idrisProofBlock start="\(default\s\+\)\?proof *{" end="}" contains=idrisTactic
lib/Builtins.idr+6
@@ -127,6 +127,12 @@ instance Eq Char where
127instance Eq String where
127instance Eq String where
128 (==) = boolOp prim__eqString
128 (==) = boolOp prim__eqString
129
129
130+instance Eq Bool where
131+ True == True = True
132+ True == False = False
133+ False == True = False
134+ False == False = True
135+
130instance (Eq a, Eq b) => Eq (a, b) where
136instance (Eq a, Eq b) => Eq (a, b) where
131 (==) (a, c) (b, d) = (a == b) && (c == d)
137 (==) (a, c) (b, d) = (a == b) && (c == d)
132
138