eea2d4a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #83 from raichoo/master

vim adjustments and Eq Bool instance

commiteea2d4afef0bd69ba0ce77161424fe2e6e555624 authorEdwin Brady <edwin.brady@gmail.com> dateThu 15 Nov 2012, 04:57 (14 years ago) parenta777c93 9ae8e39

2 files changed+8−2

compare with master

unifiedsplit

contribs/tool-support/vim/syntax/idris.vim+2−2 lib/Builtins.idr+6

contribs/tool-support/vim/syntax/idris.vim+2−2

@@ -10,7 +10,7 @@ syn match idrisModule "\<$module\|namespace$\>"

1010syn match idrisImport "\<import\>"

1111syn match idrisStructure "\<$class\|\(co$\?data\|instance\|where\|record\)\>"

1212syn match idrisVisibility "\<$public\|abstract\|private$\>"

1414syn match idrisSyntax "$pattern \+\|term \+$\?syntax"

1515syn match idrisConditional "\<$if\|then\|else$\>"

@@ -23,7 +23,7 @@ syn match idrisType "\<$[A-Z][a-zA-Z0-9_]*\|_|_$\>"

2323syn match idrisLineComment "---*$[^-!#$%&\*\+./<=>\?@\\^|~].*$\?$"

2424syn match idrisMetaVar "?[a-z][A-Za-z0-9_]\+"

2525syn match idrisLink "%$lib\|link\|include$"

26−syn match idrisDirective "%$access\|default$"

26+syn match idrisDirective "%$access\|default\|assert_total$"

2727syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+

2828syn region idrisBlockComment start="{-" end="-}"

2929syn region idrisProofBlock start="$default\s\+$\?proof *{" end="}" contains=idrisTactic

lib/Builtins.idr+6

@@ -127,6 +127,12 @@ instance Eq Char where

127127instance Eq String where

128128 (==) = boolOp prim__eqString

129129

130+instance Eq Bool where

131+ True == True = True

132+ True == False = False

133+ False == True = False

134+ False == False = True

135+

130136instance (Eq a, Eq b) => Eq (a, b) where

131137 (==) (a, c) (b, d) = (a == b) && (c == d)

132138