mirror of
https://github.com/KevinMidboe/linguist.git
synced 2026-01-01 23:16:16 +00:00
Merge remote-tracking branch 'upstream/master' into nvidia-cuda
# Please enter a commit message to explain why this merge is necessary, # especially if it merges an updated upstream into a topic branch. # # Lines starting with '#' will be ignored, and an empty message aborts # the commit.
This commit is contained in:
Kashif Rasul
@@ -67,7 +67,11 @@ Ada:
|
||||
primary_extension: .adb
|
||||
extensions:
|
||||
- .ads
|
||||
|
||||
|
||||
Agda:
|
||||
type: programming
|
||||
primary_extension: .agda
|
||||
|
||||
ApacheConf:
|
||||
type: markup
|
||||
aliases:
|
||||
@@ -123,6 +127,7 @@ Awk:
|
||||
lexer: Awk
|
||||
primary_extension: .awk
|
||||
extensions:
|
||||
- .auk
|
||||
- .gawk
|
||||
- .mawk
|
||||
- .nawk
|
||||
@@ -437,6 +442,8 @@ Emacs Lisp:
|
||||
- elisp
|
||||
- emacs
|
||||
primary_extension: .el
|
||||
filenames:
|
||||
- .emacs
|
||||
extensions:
|
||||
- .emacs
|
||||
|
||||
@@ -794,7 +801,6 @@ LLVM:
|
||||
Lasso:
|
||||
type: programming
|
||||
lexer: Lasso
|
||||
ace_mode: lasso
|
||||
color: "#2584c3"
|
||||
primary_extension: .lasso
|
||||
|
||||
@@ -802,7 +808,6 @@ Less:
|
||||
type: markup
|
||||
group: CSS
|
||||
lexer: CSS
|
||||
ace_mode: less
|
||||
primary_extension: .less
|
||||
|
||||
LilyPond:
|
||||
@@ -811,6 +816,13 @@ LilyPond:
|
||||
extensions:
|
||||
- .ily
|
||||
|
||||
Literate Agda:
|
||||
type: programming
|
||||
group: Agda
|
||||
primary_extension: .lagda
|
||||
extensions:
|
||||
- .lagda
|
||||
|
||||
Literate CoffeeScript:
|
||||
type: programming
|
||||
group: CoffeeScript
|
||||
|
||||
@@ -3,6 +3,9 @@
|
||||
"ABAP": [
|
||||
".abap"
|
||||
],
|
||||
"Agda": [
|
||||
".agda"
|
||||
],
|
||||
"Apex": [
|
||||
".cls"
|
||||
],
|
||||
@@ -35,6 +38,15 @@
|
||||
"Ceylon": [
|
||||
".ceylon"
|
||||
],
|
||||
"Clojure": [
|
||||
".cl2",
|
||||
".clj",
|
||||
".cljc",
|
||||
".cljs",
|
||||
".cljscm",
|
||||
".cljx",
|
||||
".hic"
|
||||
],
|
||||
"COBOL": [
|
||||
".cbl",
|
||||
".ccp",
|
||||
@@ -59,6 +71,9 @@
|
||||
"Diff": [
|
||||
".patch"
|
||||
],
|
||||
"DM": [
|
||||
".dm"
|
||||
],
|
||||
"Ecl": [
|
||||
".ecl"
|
||||
],
|
||||
@@ -111,9 +126,15 @@
|
||||
".handlebars",
|
||||
".hbs"
|
||||
],
|
||||
"Idris": [
|
||||
".idr"
|
||||
],
|
||||
"Ioke": [
|
||||
".ik"
|
||||
],
|
||||
"Jade": [
|
||||
".jade"
|
||||
],
|
||||
"Java": [
|
||||
".java"
|
||||
],
|
||||
@@ -132,6 +153,9 @@
|
||||
"Kotlin": [
|
||||
".kt"
|
||||
],
|
||||
"KRL": [
|
||||
".krl"
|
||||
],
|
||||
"Lasso": [
|
||||
".las",
|
||||
".lasso",
|
||||
@@ -144,6 +168,9 @@
|
||||
"LFE": [
|
||||
".lfe"
|
||||
],
|
||||
"Literate Agda": [
|
||||
".lagda"
|
||||
],
|
||||
"Literate CoffeeScript": [
|
||||
".litcoffee"
|
||||
],
|
||||
@@ -249,6 +276,9 @@
|
||||
"Prolog": [
|
||||
".pl"
|
||||
],
|
||||
"Protocol Buffer": [
|
||||
".proto"
|
||||
],
|
||||
"Python": [
|
||||
".py",
|
||||
".script!"
|
||||
@@ -267,6 +297,9 @@
|
||||
"Rebol": [
|
||||
".r"
|
||||
],
|
||||
"RobotFramework": [
|
||||
".robot"
|
||||
],
|
||||
"Ruby": [
|
||||
".pluginspec",
|
||||
".rabl",
|
||||
@@ -285,6 +318,9 @@
|
||||
".sbt",
|
||||
".script!"
|
||||
],
|
||||
"Scaml": [
|
||||
".scaml"
|
||||
],
|
||||
"Scheme": [
|
||||
".sps"
|
||||
],
|
||||
@@ -424,8 +460,8 @@
|
||||
".gemrc"
|
||||
]
|
||||
},
|
||||
"tokens_total": 415313,
|
||||
"languages_total": 458,
|
||||
"tokens_total": 417572,
|
||||
"languages_total": 476,
|
||||
"tokens": {
|
||||
"ABAP": {
|
||||
"*/**": 1,
|
||||
@@ -686,6 +722,64 @@
|
||||
"pos": 2,
|
||||
"endclass.": 1
|
||||
},
|
||||
"Agda": {
|
||||
"module": 3,
|
||||
"NatCat": 1,
|
||||
"where": 2,
|
||||
"open": 2,
|
||||
"import": 2,
|
||||
"Relation.Binary.PropositionalEquality": 1,
|
||||
"-": 21,
|
||||
"If": 1,
|
||||
"you": 2,
|
||||
"can": 1,
|
||||
"show": 1,
|
||||
"that": 1,
|
||||
"a": 1,
|
||||
"relation": 1,
|
||||
"only": 1,
|
||||
"ever": 1,
|
||||
"has": 1,
|
||||
"one": 1,
|
||||
"inhabitant": 5,
|
||||
"get": 1,
|
||||
"the": 1,
|
||||
"category": 1,
|
||||
"laws": 1,
|
||||
"for": 1,
|
||||
"free": 1,
|
||||
"EasyCategory": 3,
|
||||
"(": 36,
|
||||
"obj": 4,
|
||||
"Set": 2,
|
||||
")": 36,
|
||||
"_": 6,
|
||||
"{": 10,
|
||||
"x": 34,
|
||||
"y": 28,
|
||||
"z": 18,
|
||||
"}": 10,
|
||||
"id": 9,
|
||||
"single": 4,
|
||||
"r": 26,
|
||||
"s": 29,
|
||||
"assoc": 2,
|
||||
"w": 4,
|
||||
"t": 6,
|
||||
"Data.Nat": 1,
|
||||
"same": 5,
|
||||
".0": 2,
|
||||
"n": 14,
|
||||
"refl": 6,
|
||||
".": 5,
|
||||
"suc": 6,
|
||||
"m": 6,
|
||||
"cong": 1,
|
||||
"trans": 5,
|
||||
".n": 1,
|
||||
"zero": 1,
|
||||
"Nat": 1
|
||||
},
|
||||
"ApacheConf": {
|
||||
"ServerSignature": 1,
|
||||
"Off": 1,
|
||||
@@ -10087,6 +10181,136 @@
|
||||
"<=>": 1,
|
||||
"other.name": 1
|
||||
},
|
||||
"Clojure": {
|
||||
"(": 83,
|
||||
"defn": 4,
|
||||
"prime": 2,
|
||||
"[": 41,
|
||||
"n": 9,
|
||||
"]": 41,
|
||||
"not": 3,
|
||||
"-": 14,
|
||||
"any": 1,
|
||||
"zero": 1,
|
||||
"map": 2,
|
||||
"#": 1,
|
||||
"rem": 2,
|
||||
"%": 1,
|
||||
")": 84,
|
||||
"range": 3,
|
||||
";": 8,
|
||||
"while": 3,
|
||||
"stops": 1,
|
||||
"at": 1,
|
||||
"the": 1,
|
||||
"first": 2,
|
||||
"collection": 1,
|
||||
"element": 1,
|
||||
"that": 1,
|
||||
"evaluates": 1,
|
||||
"to": 1,
|
||||
"false": 2,
|
||||
"like": 1,
|
||||
"take": 1,
|
||||
"for": 2,
|
||||
"x": 6,
|
||||
"html": 1,
|
||||
"head": 1,
|
||||
"meta": 1,
|
||||
"{": 8,
|
||||
"charset": 1,
|
||||
"}": 8,
|
||||
"link": 1,
|
||||
"rel": 1,
|
||||
"href": 1,
|
||||
"script": 1,
|
||||
"src": 1,
|
||||
"body": 1,
|
||||
"div.nav": 1,
|
||||
"p": 1,
|
||||
"into": 2,
|
||||
"array": 3,
|
||||
"aseq": 8,
|
||||
"nil": 1,
|
||||
"type": 2,
|
||||
"let": 1,
|
||||
"count": 3,
|
||||
"a": 3,
|
||||
"make": 1,
|
||||
"loop": 1,
|
||||
"seq": 1,
|
||||
"i": 4,
|
||||
"if": 1,
|
||||
"<": 1,
|
||||
"do": 1,
|
||||
"aset": 1,
|
||||
"recur": 1,
|
||||
"next": 1,
|
||||
"inc": 1,
|
||||
"defprotocol": 1,
|
||||
"ISound": 4,
|
||||
"sound": 5,
|
||||
"deftype": 2,
|
||||
"Cat": 1,
|
||||
"_": 3,
|
||||
"Dog": 1,
|
||||
"extend": 1,
|
||||
"default": 1,
|
||||
"rand": 2,
|
||||
"scm*": 1,
|
||||
"random": 1,
|
||||
"real": 1,
|
||||
"clj": 1,
|
||||
"ns": 2,
|
||||
"c2.svg": 2,
|
||||
"use": 2,
|
||||
"c2.core": 2,
|
||||
"only": 4,
|
||||
"unify": 2,
|
||||
"c2.maths": 2,
|
||||
"Pi": 2,
|
||||
"Tau": 2,
|
||||
"radians": 2,
|
||||
"per": 2,
|
||||
"degree": 2,
|
||||
"sin": 2,
|
||||
"cos": 2,
|
||||
"mean": 2,
|
||||
"cljs": 3,
|
||||
"require": 1,
|
||||
"c2.dom": 1,
|
||||
"as": 1,
|
||||
"dom": 1,
|
||||
"Stub": 1,
|
||||
"float": 2,
|
||||
"fn": 2,
|
||||
"which": 1,
|
||||
"does": 1,
|
||||
"exist": 1,
|
||||
"on": 1,
|
||||
"runtime": 1,
|
||||
"def": 1,
|
||||
"identity": 1,
|
||||
"xy": 1,
|
||||
"coordinates": 7,
|
||||
"cond": 1,
|
||||
"and": 1,
|
||||
"vector": 1,
|
||||
"y": 1,
|
||||
"deftest": 1,
|
||||
"function": 1,
|
||||
"tests": 1,
|
||||
"is": 7,
|
||||
"true": 2,
|
||||
"contains": 1,
|
||||
"foo": 6,
|
||||
"bar": 4,
|
||||
"select": 1,
|
||||
"keys": 2,
|
||||
"baz": 4,
|
||||
"vals": 1,
|
||||
"filter": 1
|
||||
},
|
||||
"COBOL": {
|
||||
"program": 1,
|
||||
"-": 19,
|
||||
@@ -13002,6 +13226,98 @@
|
||||
"d472341..8ad9ffb": 1,
|
||||
"+": 3
|
||||
},
|
||||
"DM": {
|
||||
"#define": 4,
|
||||
"PI": 6,
|
||||
"#if": 1,
|
||||
"G": 1,
|
||||
"#elif": 1,
|
||||
"I": 1,
|
||||
"#else": 1,
|
||||
"K": 1,
|
||||
"#endif": 1,
|
||||
"var/GlobalCounter": 1,
|
||||
"var/const/CONST_VARIABLE": 1,
|
||||
"var/list/MyList": 1,
|
||||
"list": 3,
|
||||
"(": 17,
|
||||
"new": 1,
|
||||
"/datum/entity": 2,
|
||||
")": 17,
|
||||
"var/list/EmptyList": 1,
|
||||
"[": 2,
|
||||
"]": 2,
|
||||
"//": 6,
|
||||
"creates": 1,
|
||||
"a": 1,
|
||||
"of": 1,
|
||||
"null": 2,
|
||||
"entries": 1,
|
||||
"var/list/NullList": 1,
|
||||
"var/name": 1,
|
||||
"var/number": 1,
|
||||
"/datum/entity/proc/myFunction": 1,
|
||||
"world.log": 5,
|
||||
"<<": 5,
|
||||
"/datum/entity/New": 1,
|
||||
"number": 2,
|
||||
"GlobalCounter": 1,
|
||||
"+": 3,
|
||||
"/datum/entity/unit": 1,
|
||||
"name": 1,
|
||||
"/datum/entity/unit/New": 1,
|
||||
"..": 1,
|
||||
"calls": 1,
|
||||
"the": 2,
|
||||
"parent": 1,
|
||||
"s": 1,
|
||||
"proc": 1,
|
||||
";": 3,
|
||||
"equal": 1,
|
||||
"to": 1,
|
||||
"super": 1,
|
||||
"and": 1,
|
||||
"base": 1,
|
||||
"in": 1,
|
||||
"other": 1,
|
||||
"languages": 1,
|
||||
"rand": 1,
|
||||
"/datum/entity/unit/myFunction": 1,
|
||||
"/proc/ReverseList": 1,
|
||||
"var/list/input": 1,
|
||||
"var/list/output": 1,
|
||||
"for": 1,
|
||||
"var/i": 1,
|
||||
"input.len": 1,
|
||||
"i": 3,
|
||||
"-": 2,
|
||||
"IMPORTANT": 1,
|
||||
"List": 1,
|
||||
"Arrays": 1,
|
||||
"count": 1,
|
||||
"from": 1,
|
||||
"output": 2,
|
||||
"input": 1,
|
||||
"is": 2,
|
||||
"return": 3,
|
||||
"/proc/DoStuff": 1,
|
||||
"var/bitflag": 2,
|
||||
"bitflag": 4,
|
||||
"|": 1,
|
||||
"/proc/DoOtherStuff": 1,
|
||||
"bits": 1,
|
||||
"maximum": 1,
|
||||
"amount": 1,
|
||||
"&": 1,
|
||||
"/proc/DoNothing": 1,
|
||||
"var/pi": 1,
|
||||
"if": 2,
|
||||
"pi": 2,
|
||||
"else": 2,
|
||||
"CONST_VARIABLE": 1,
|
||||
"#undef": 1,
|
||||
"Undefine": 1
|
||||
},
|
||||
"Ecl": {
|
||||
"#option": 1,
|
||||
"(": 32,
|
||||
@@ -15176,6 +15492,46 @@
|
||||
"</h2>": 1,
|
||||
"/each": 1
|
||||
},
|
||||
"Idris": {
|
||||
"module": 1,
|
||||
"Prelude.Char": 1,
|
||||
"import": 1,
|
||||
"Builtins": 1,
|
||||
"isUpper": 4,
|
||||
"Char": 13,
|
||||
"-": 8,
|
||||
"Bool": 8,
|
||||
"x": 36,
|
||||
"&&": 3,
|
||||
"<=>": 3,
|
||||
"Z": 1,
|
||||
"isLower": 4,
|
||||
"z": 1,
|
||||
"isAlpha": 3,
|
||||
"||": 9,
|
||||
"isDigit": 3,
|
||||
"(": 8,
|
||||
"9": 1,
|
||||
"isAlphaNum": 2,
|
||||
"isSpace": 2,
|
||||
"isNL": 2,
|
||||
"toUpper": 3,
|
||||
"if": 2,
|
||||
")": 7,
|
||||
"then": 2,
|
||||
"prim__intToChar": 2,
|
||||
"prim__charToInt": 2,
|
||||
"else": 2,
|
||||
"toLower": 2,
|
||||
"+": 1,
|
||||
"isHexDigit": 2,
|
||||
"elem": 1,
|
||||
"hexChars": 3,
|
||||
"where": 1,
|
||||
"List": 1,
|
||||
"[": 1,
|
||||
"]": 1
|
||||
},
|
||||
"INI": {
|
||||
";": 1,
|
||||
"editorconfig.org": 1,
|
||||
@@ -15205,6 +15561,11 @@
|
||||
"SHEBANG#!ioke": 1,
|
||||
"println": 1
|
||||
},
|
||||
"Jade": {
|
||||
"p.": 1,
|
||||
"Hello": 1,
|
||||
"World": 1
|
||||
},
|
||||
"Java": {
|
||||
"package": 6,
|
||||
"clojure.asm": 1,
|
||||
@@ -22324,6 +22685,29 @@
|
||||
"true": 1,
|
||||
"return": 1
|
||||
},
|
||||
"KRL": {
|
||||
"ruleset": 1,
|
||||
"sample": 1,
|
||||
"{": 3,
|
||||
"meta": 1,
|
||||
"name": 1,
|
||||
"description": 1,
|
||||
"<<": 1,
|
||||
"Hello": 1,
|
||||
"world": 1,
|
||||
"author": 1,
|
||||
"}": 3,
|
||||
"rule": 1,
|
||||
"hello": 1,
|
||||
"select": 1,
|
||||
"when": 1,
|
||||
"web": 1,
|
||||
"pageview": 1,
|
||||
"notify": 1,
|
||||
"(": 1,
|
||||
")": 1,
|
||||
";": 1
|
||||
},
|
||||
"Lasso": {
|
||||
"<": 7,
|
||||
"LassoScript": 1,
|
||||
@@ -23542,6 +23926,98 @@
|
||||
"info": 1,
|
||||
"reproduce": 1
|
||||
},
|
||||
"Literate Agda": {
|
||||
"documentclass": 1,
|
||||
"{": 35,
|
||||
"article": 1,
|
||||
"}": 35,
|
||||
"usepackage": 7,
|
||||
"amssymb": 1,
|
||||
"bbm": 1,
|
||||
"[": 2,
|
||||
"greek": 1,
|
||||
"english": 1,
|
||||
"]": 2,
|
||||
"babel": 1,
|
||||
"ucs": 1,
|
||||
"utf8x": 1,
|
||||
"inputenc": 1,
|
||||
"autofe": 1,
|
||||
"DeclareUnicodeCharacter": 3,
|
||||
"ensuremath": 3,
|
||||
"ulcorner": 1,
|
||||
"urcorner": 1,
|
||||
"overline": 1,
|
||||
"equiv": 1,
|
||||
"fancyvrb": 1,
|
||||
"DefineVerbatimEnvironment": 1,
|
||||
"code": 3,
|
||||
"Verbatim": 1,
|
||||
"%": 1,
|
||||
"Add": 1,
|
||||
"fancy": 1,
|
||||
"options": 1,
|
||||
"here": 1,
|
||||
"if": 1,
|
||||
"you": 3,
|
||||
"like.": 1,
|
||||
"begin": 2,
|
||||
"document": 2,
|
||||
"module": 3,
|
||||
"NatCat": 1,
|
||||
"where": 2,
|
||||
"open": 2,
|
||||
"import": 2,
|
||||
"Relation.Binary.PropositionalEquality": 1,
|
||||
"-": 21,
|
||||
"If": 1,
|
||||
"can": 1,
|
||||
"show": 1,
|
||||
"that": 1,
|
||||
"a": 1,
|
||||
"relation": 1,
|
||||
"only": 1,
|
||||
"ever": 1,
|
||||
"has": 1,
|
||||
"one": 1,
|
||||
"inhabitant": 5,
|
||||
"get": 1,
|
||||
"the": 1,
|
||||
"category": 1,
|
||||
"laws": 1,
|
||||
"for": 1,
|
||||
"free": 1,
|
||||
"EasyCategory": 3,
|
||||
"(": 36,
|
||||
"obj": 4,
|
||||
"Set": 2,
|
||||
")": 36,
|
||||
"_": 6,
|
||||
"x": 34,
|
||||
"y": 28,
|
||||
"z": 18,
|
||||
"id": 9,
|
||||
"single": 4,
|
||||
"r": 26,
|
||||
"s": 29,
|
||||
"assoc": 2,
|
||||
"w": 4,
|
||||
"t": 6,
|
||||
"Data.Nat": 1,
|
||||
"same": 5,
|
||||
".0": 2,
|
||||
"n": 14,
|
||||
"refl": 6,
|
||||
".": 5,
|
||||
"suc": 6,
|
||||
"m": 6,
|
||||
"cong": 1,
|
||||
"trans": 5,
|
||||
".n": 1,
|
||||
"zero": 1,
|
||||
"Nat": 1,
|
||||
"end": 2
|
||||
},
|
||||
"Literate CoffeeScript": {
|
||||
"The": 2,
|
||||
"**Scope**": 2,
|
||||
@@ -34694,6 +35170,40 @@
|
||||
"stay": 1,
|
||||
"L": 2
|
||||
},
|
||||
"Protocol Buffer": {
|
||||
"package": 1,
|
||||
"tutorial": 1,
|
||||
";": 13,
|
||||
"option": 2,
|
||||
"java_package": 1,
|
||||
"java_outer_classname": 1,
|
||||
"message": 3,
|
||||
"Person": 2,
|
||||
"{": 4,
|
||||
"required": 3,
|
||||
"string": 3,
|
||||
"name": 1,
|
||||
"int32": 1,
|
||||
"id": 1,
|
||||
"optional": 2,
|
||||
"email": 1,
|
||||
"enum": 1,
|
||||
"PhoneType": 2,
|
||||
"MOBILE": 1,
|
||||
"HOME": 2,
|
||||
"WORK": 1,
|
||||
"}": 4,
|
||||
"PhoneNumber": 2,
|
||||
"number": 1,
|
||||
"type": 1,
|
||||
"[": 1,
|
||||
"default": 1,
|
||||
"]": 1,
|
||||
"repeated": 2,
|
||||
"phone": 1,
|
||||
"AddressBook": 1,
|
||||
"person": 1
|
||||
},
|
||||
"Python": {
|
||||
"from": 34,
|
||||
"__future__": 2,
|
||||
@@ -35972,6 +36482,193 @@
|
||||
"func": 1,
|
||||
"print": 1
|
||||
},
|
||||
"RobotFramework": {
|
||||
"***": 16,
|
||||
"Settings": 3,
|
||||
"Documentation": 3,
|
||||
"Example": 3,
|
||||
"test": 6,
|
||||
"cases": 2,
|
||||
"using": 4,
|
||||
"the": 9,
|
||||
"data": 2,
|
||||
"-": 16,
|
||||
"driven": 4,
|
||||
"testing": 2,
|
||||
"approach.": 2,
|
||||
"...": 28,
|
||||
"Tests": 1,
|
||||
"use": 2,
|
||||
"Calculate": 3,
|
||||
"keyword": 5,
|
||||
"created": 1,
|
||||
"in": 5,
|
||||
"this": 1,
|
||||
"file": 1,
|
||||
"that": 5,
|
||||
"turn": 1,
|
||||
"uses": 1,
|
||||
"keywords": 3,
|
||||
"CalculatorLibrary": 5,
|
||||
".": 4,
|
||||
"An": 1,
|
||||
"exception": 1,
|
||||
"is": 6,
|
||||
"last": 1,
|
||||
"has": 5,
|
||||
"a": 4,
|
||||
"custom": 1,
|
||||
"_template": 1,
|
||||
"keyword_.": 1,
|
||||
"The": 2,
|
||||
"style": 3,
|
||||
"works": 3,
|
||||
"well": 3,
|
||||
"when": 2,
|
||||
"you": 1,
|
||||
"need": 3,
|
||||
"to": 5,
|
||||
"repeat": 1,
|
||||
"same": 1,
|
||||
"workflow": 3,
|
||||
"multiple": 2,
|
||||
"times.": 1,
|
||||
"Notice": 1,
|
||||
"one": 1,
|
||||
"of": 3,
|
||||
"these": 1,
|
||||
"tests": 5,
|
||||
"fails": 1,
|
||||
"on": 1,
|
||||
"purpose": 1,
|
||||
"show": 1,
|
||||
"how": 1,
|
||||
"failures": 1,
|
||||
"look": 1,
|
||||
"like.": 1,
|
||||
"Test": 4,
|
||||
"Template": 2,
|
||||
"Library": 3,
|
||||
"Cases": 3,
|
||||
"Expression": 1,
|
||||
"Expected": 1,
|
||||
"Addition": 2,
|
||||
"+": 6,
|
||||
"Subtraction": 1,
|
||||
"Multiplication": 1,
|
||||
"*": 4,
|
||||
"Division": 2,
|
||||
"/": 5,
|
||||
"Failing": 1,
|
||||
"Calculation": 3,
|
||||
"error": 4,
|
||||
"[": 4,
|
||||
"]": 4,
|
||||
"should": 9,
|
||||
"fail": 2,
|
||||
"kekkonen": 1,
|
||||
"Invalid": 2,
|
||||
"button": 13,
|
||||
"{": 15,
|
||||
"EMPTY": 3,
|
||||
"}": 15,
|
||||
"expression.": 1,
|
||||
"by": 3,
|
||||
"zero.": 1,
|
||||
"Keywords": 2,
|
||||
"Arguments": 2,
|
||||
"expression": 5,
|
||||
"expected": 4,
|
||||
"Push": 16,
|
||||
"buttons": 4,
|
||||
"C": 4,
|
||||
"Result": 8,
|
||||
"be": 9,
|
||||
"Should": 2,
|
||||
"cause": 1,
|
||||
"equal": 1,
|
||||
"#": 2,
|
||||
"Using": 1,
|
||||
"BuiltIn": 1,
|
||||
"case": 1,
|
||||
"gherkin": 1,
|
||||
"syntax.": 1,
|
||||
"This": 3,
|
||||
"similar": 1,
|
||||
"examples.": 1,
|
||||
"difference": 1,
|
||||
"higher": 1,
|
||||
"abstraction": 1,
|
||||
"level": 1,
|
||||
"and": 2,
|
||||
"their": 1,
|
||||
"arguments": 1,
|
||||
"are": 1,
|
||||
"embedded": 1,
|
||||
"into": 1,
|
||||
"names.": 1,
|
||||
"kind": 2,
|
||||
"_gherkin_": 2,
|
||||
"syntax": 1,
|
||||
"been": 3,
|
||||
"made": 1,
|
||||
"popular": 1,
|
||||
"http": 1,
|
||||
"//cukes.info": 1,
|
||||
"|": 1,
|
||||
"Cucumber": 1,
|
||||
"It": 1,
|
||||
"especially": 1,
|
||||
"act": 1,
|
||||
"as": 1,
|
||||
"examples": 1,
|
||||
"easily": 1,
|
||||
"understood": 1,
|
||||
"also": 2,
|
||||
"business": 2,
|
||||
"people.": 1,
|
||||
"Given": 1,
|
||||
"calculator": 1,
|
||||
"cleared": 2,
|
||||
"When": 1,
|
||||
"user": 2,
|
||||
"types": 2,
|
||||
"pushes": 2,
|
||||
"equals": 2,
|
||||
"Then": 1,
|
||||
"result": 2,
|
||||
"Calculator": 1,
|
||||
"User": 2,
|
||||
"All": 1,
|
||||
"contain": 1,
|
||||
"constructed": 1,
|
||||
"from": 1,
|
||||
"Creating": 1,
|
||||
"new": 1,
|
||||
"or": 1,
|
||||
"editing": 1,
|
||||
"existing": 1,
|
||||
"easy": 1,
|
||||
"even": 1,
|
||||
"for": 2,
|
||||
"people": 2,
|
||||
"without": 1,
|
||||
"programming": 1,
|
||||
"skills.": 1,
|
||||
"normal": 1,
|
||||
"automation.": 1,
|
||||
"If": 1,
|
||||
"understand": 1,
|
||||
"may": 1,
|
||||
"work": 1,
|
||||
"better.": 1,
|
||||
"Simple": 1,
|
||||
"calculation": 2,
|
||||
"Longer": 1,
|
||||
"Clear": 1,
|
||||
"built": 1,
|
||||
"variable": 1
|
||||
},
|
||||
"Ruby": {
|
||||
"load": 3,
|
||||
"Dir": 4,
|
||||
@@ -37563,6 +38260,12 @@
|
||||
"[": 1,
|
||||
"]": 1
|
||||
},
|
||||
"Scaml": {
|
||||
"%": 1,
|
||||
"p": 1,
|
||||
"Hello": 1,
|
||||
"World": 1
|
||||
},
|
||||
"Scheme": {
|
||||
"(": 359,
|
||||
"import": 1,
|
||||
@@ -41521,6 +42224,7 @@
|
||||
},
|
||||
"language_tokens": {
|
||||
"ABAP": 1500,
|
||||
"Agda": 376,
|
||||
"ApacheConf": 1449,
|
||||
"Apex": 4408,
|
||||
"AppleScript": 1862,
|
||||
@@ -41531,6 +42235,7 @@
|
||||
"C": 58858,
|
||||
"C++": 21480,
|
||||
"Ceylon": 50,
|
||||
"Clojure": 510,
|
||||
"COBOL": 90,
|
||||
"CoffeeScript": 2951,
|
||||
"Common Lisp": 103,
|
||||
@@ -41538,6 +42243,7 @@
|
||||
"CSS": 43867,
|
||||
"Dart": 68,
|
||||
"Diff": 16,
|
||||
"DM": 169,
|
||||
"Ecl": 281,
|
||||
"edn": 227,
|
||||
"Elm": 628,
|
||||
@@ -41552,16 +42258,20 @@
|
||||
"Groovy Server Pages": 91,
|
||||
"Haml": 4,
|
||||
"Handlebars": 69,
|
||||
"Idris": 148,
|
||||
"INI": 27,
|
||||
"Ioke": 2,
|
||||
"Jade": 3,
|
||||
"Java": 8987,
|
||||
"JavaScript": 76934,
|
||||
"JSON": 619,
|
||||
"Julia": 247,
|
||||
"Kotlin": 155,
|
||||
"KRL": 25,
|
||||
"Lasso": 9849,
|
||||
"Less": 39,
|
||||
"LFE": 1711,
|
||||
"Literate Agda": 478,
|
||||
"Literate CoffeeScript": 275,
|
||||
"LiveScript": 123,
|
||||
"Logos": 93,
|
||||
@@ -41594,15 +42304,18 @@
|
||||
"PowerShell": 12,
|
||||
"Processing": 74,
|
||||
"Prolog": 4040,
|
||||
"Protocol Buffer": 63,
|
||||
"Python": 5715,
|
||||
"R": 175,
|
||||
"Racket": 360,
|
||||
"Ragel in Ruby Host": 593,
|
||||
"Rebol": 11,
|
||||
"RobotFramework": 483,
|
||||
"Ruby": 3854,
|
||||
"Rust": 3566,
|
||||
"Sass": 56,
|
||||
"Scala": 420,
|
||||
"Scaml": 4,
|
||||
"Scheme": 3478,
|
||||
"Scilab": 69,
|
||||
"SCSS": 39,
|
||||
@@ -41632,6 +42345,7 @@
|
||||
},
|
||||
"languages": {
|
||||
"ABAP": 1,
|
||||
"Agda": 1,
|
||||
"ApacheConf": 3,
|
||||
"Apex": 6,
|
||||
"AppleScript": 7,
|
||||
@@ -41642,6 +42356,7 @@
|
||||
"C": 26,
|
||||
"C++": 20,
|
||||
"Ceylon": 1,
|
||||
"Clojure": 7,
|
||||
"COBOL": 4,
|
||||
"CoffeeScript": 9,
|
||||
"Common Lisp": 1,
|
||||
@@ -41649,6 +42364,7 @@
|
||||
"CSS": 2,
|
||||
"Dart": 1,
|
||||
"Diff": 1,
|
||||
"DM": 1,
|
||||
"Ecl": 1,
|
||||
"edn": 1,
|
||||
"Elm": 3,
|
||||
@@ -41663,16 +42379,20 @@
|
||||
"Groovy Server Pages": 4,
|
||||
"Haml": 1,
|
||||
"Handlebars": 2,
|
||||
"Idris": 1,
|
||||
"INI": 2,
|
||||
"Ioke": 1,
|
||||
"Jade": 1,
|
||||
"Java": 6,
|
||||
"JavaScript": 20,
|
||||
"JSON": 5,
|
||||
"Julia": 1,
|
||||
"Kotlin": 1,
|
||||
"KRL": 1,
|
||||
"Lasso": 4,
|
||||
"Less": 1,
|
||||
"LFE": 4,
|
||||
"Literate Agda": 1,
|
||||
"Literate CoffeeScript": 1,
|
||||
"LiveScript": 1,
|
||||
"Logos": 1,
|
||||
@@ -41705,15 +42425,18 @@
|
||||
"PowerShell": 2,
|
||||
"Processing": 1,
|
||||
"Prolog": 6,
|
||||
"Protocol Buffer": 1,
|
||||
"Python": 7,
|
||||
"R": 2,
|
||||
"Racket": 3,
|
||||
"Ragel in Ruby Host": 3,
|
||||
"Rebol": 1,
|
||||
"RobotFramework": 3,
|
||||
"Ruby": 16,
|
||||
"Rust": 1,
|
||||
"Sass": 2,
|
||||
"Scala": 3,
|
||||
"Scaml": 1,
|
||||
"Scheme": 1,
|
||||
"Scilab": 3,
|
||||
"SCSS": 1,
|
||||
@@ -41741,5 +42464,5 @@
|
||||
"Xtend": 2,
|
||||
"YAML": 1
|
||||
},
|
||||
"md5": "e1daa29f986e203ade56a02091d24c99"
|
||||
"md5": "6a064f3fdb191614ff6f065a365cb3d7"
|
||||
}
|
||||
39
samples/Agda/NatCat.agda
Normal file
39
samples/Agda/NatCat.agda
Normal file
@@ -0,0 +1,39 @@
|
||||
module NatCat where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
|
||||
-- If you can show that a relation only ever has one inhabitant
|
||||
-- you get the category laws for free
|
||||
module
|
||||
EasyCategory
|
||||
(obj : Set)
|
||||
(_⟶_ : obj → obj → Set)
|
||||
(_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z)
|
||||
(id : ∀ x → x ⟶ x)
|
||||
(single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s)
|
||||
where
|
||||
|
||||
idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r
|
||||
idʳ x y r = single-inhabitant x y (r ∘ id y) r
|
||||
|
||||
idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r
|
||||
idˡ x y r = single-inhabitant x y (id x ∘ r) r
|
||||
|
||||
∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t)
|
||||
∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t))
|
||||
|
||||
open import Data.Nat
|
||||
|
||||
same : (x y : ℕ) (r s : x ≤ y) → r ≡ s
|
||||
same .0 y z≤n z≤n = refl
|
||||
same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s)
|
||||
|
||||
≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
|
||||
≤-trans .0 y z z≤n s = z≤n
|
||||
≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s)
|
||||
|
||||
≤-refl : ∀ x → x ≤ x
|
||||
≤-refl zero = z≤n
|
||||
≤-refl (suc x) = s≤s (≤-refl x)
|
||||
|
||||
module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same
|
||||
82
samples/Literate Agda/NatCat.lagda
Normal file
82
samples/Literate Agda/NatCat.lagda
Normal file
@@ -0,0 +1,82 @@
|
||||
\documentclass{article}
|
||||
|
||||
% The following packages are needed because unicode
|
||||
% is translated (using the next set of packages) to
|
||||
% latex commands. You may need more packages if you
|
||||
% use more unicode characters:
|
||||
|
||||
\usepackage{amssymb}
|
||||
\usepackage{bbm}
|
||||
\usepackage[greek,english]{babel}
|
||||
|
||||
% This handles the translation of unicode to latex:
|
||||
|
||||
\usepackage{ucs}
|
||||
\usepackage[utf8x]{inputenc}
|
||||
\usepackage{autofe}
|
||||
|
||||
% Some characters that are not automatically defined
|
||||
% (you figure out by the latex compilation errors you get),
|
||||
% and you need to define:
|
||||
|
||||
\DeclareUnicodeCharacter{8988}{\ensuremath{\ulcorner}}
|
||||
\DeclareUnicodeCharacter{8989}{\ensuremath{\urcorner}}
|
||||
\DeclareUnicodeCharacter{8803}{\ensuremath{\overline{\equiv}}}
|
||||
|
||||
% Add more as you need them (shouldn’t happen often).
|
||||
|
||||
% Using “\newenvironment” to redefine verbatim to
|
||||
% be called “code” doesn’t always work properly.
|
||||
% You can more reliably use:
|
||||
|
||||
\usepackage{fancyvrb}
|
||||
|
||||
\DefineVerbatimEnvironment
|
||||
{code}{Verbatim}
|
||||
{} % Add fancy options here if you like.
|
||||
|
||||
\begin{document}
|
||||
|
||||
\begin{code}
|
||||
module NatCat where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
|
||||
-- If you can show that a relation only ever has one inhabitant
|
||||
-- you get the category laws for free
|
||||
module
|
||||
EasyCategory
|
||||
(obj : Set)
|
||||
(_⟶_ : obj → obj → Set)
|
||||
(_∘_ : ∀ {x y z} → x ⟶ y → y ⟶ z → x ⟶ z)
|
||||
(id : ∀ x → x ⟶ x)
|
||||
(single-inhabitant : (x y : obj) (r s : x ⟶ y) → r ≡ s)
|
||||
where
|
||||
|
||||
idʳ : ∀ x y (r : x ⟶ y) → r ∘ id y ≡ r
|
||||
idʳ x y r = single-inhabitant x y (r ∘ id y) r
|
||||
|
||||
idˡ : ∀ x y (r : x ⟶ y) → id x ∘ r ≡ r
|
||||
idˡ x y r = single-inhabitant x y (id x ∘ r) r
|
||||
|
||||
∘-assoc : ∀ w x y z (r : w ⟶ x) (s : x ⟶ y) (t : y ⟶ z) → (r ∘ s) ∘ t ≡ r ∘ (s ∘ t)
|
||||
∘-assoc w x y z r s t = single-inhabitant w z ((r ∘ s) ∘ t) (r ∘ (s ∘ t))
|
||||
|
||||
open import Data.Nat
|
||||
|
||||
same : (x y : ℕ) (r s : x ≤ y) → r ≡ s
|
||||
same .0 y z≤n z≤n = refl
|
||||
same .(suc m) .(suc n) (s≤s {m} {n} r) (s≤s s) = cong s≤s (same m n r s)
|
||||
|
||||
≤-trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
|
||||
≤-trans .0 y z z≤n s = z≤n
|
||||
≤-trans .(suc m) .(suc n) .(suc n₁) (s≤s {m} {n} r) (s≤s {.n} {n₁} s) = s≤s (≤-trans m n n₁ r s)
|
||||
|
||||
≤-refl : ∀ x → x ≤ x
|
||||
≤-refl zero = z≤n
|
||||
≤-refl (suc x) = s≤s (≤-refl x)
|
||||
|
||||
module Nat-EasyCategory = EasyCategory ℕ _≤_ (λ {x}{y}{z} → ≤-trans x y z) ≤-refl same
|
||||
\end{code}
|
||||
|
||||
\end{document}
|
||||
Reference in New Issue
Block a user