{
  "name": "Agda",
  "scopeName": "source.agda",
  "patterns": [
    {
      "name": "comment.line.double-dash.agda",
      "begin": "--",
      "end": "$"
    },
    {
      "name": "comment.block.agda",
      "begin": "{-[^#]",
      "end": "-}"
    },
    {
      "name": "support.other.agda",
      "begin": "{-#",
      "end": "#-}"
    },
    {
      "name": "string.quoted.double.agda",
      "begin": "\"",
      "end": "\""
    },
    {
      "name": "constant.char.agda",
      "match": "'([^\\\\']|\\\\['\\\\\"[:alnum:]]+)'"
    },
    {
      "name": "constant.numeric.agda",
      "match": "(?\u003c=^|[[:space:]\\(\\){}])(-?\\d+|0x[0-9A-F]+|-?\\d+\\.\\d+((e|E)(\\+|-)?\\d+)?|-?\\d+(e|E)(\\+|-)?\\d+)(?=[[:space:]\\(\\){}])"
    },
    {
      "match": "\\b(data|record|module|constructor|open *import|open|import)[[:space:]]+([^;\\(\\){}@\"[:space:]]+)",
      "captures": {
        "1": {
          "name": "keyword.other.agda"
        },
        "2": {
          "name": "entity.name.type.agda"
        }
      }
    },
    {
      "name": "entity.name.tag.agda",
      "match": "((?\u003c=^|[.;\\(\\){}@\"[:space:]])\\?(?=[.;\\(\\){}@\"[:space:]])|{!.*!})"
    },
    {
      "name": "constant.language.agda",
      "match": "\\b(Set|Prop)[0123456789₀₁₂₃₄₅₆₇₈₉]*(?=$|[[:space:]\\(\\)\\{\\}])"
    },
    {
      "name": "keyword.other.agda",
      "match": "(?\u003c=^|[[:space:]\\(\\)\\{\\}])(λ|→|-\u003e|∀|=|←|:)(?=[[:space:]\\(\\)\\{\\}])"
    },
    {
      "match": "^[[:space:]]*(((abstract|instance|macro|pattern|postulate|primitive|private|syntax|variable|where|let)[[:space:]]+)*)((([^;\\(\\){}@\"[:space:]]+)[[:space:]]+)+)(?=:)",
      "captures": {
        "1": {
          "name": "keyword.other.agda"
        },
        "4": {
          "name": "entity.name.agda"
        }
      }
    },
    {
      "name": "keyword.other.agda",
      "match": "(?\u003c=^|[[:space:]\\(\\){}])(abstract|constructor|data|do|eta-equality|field|forall|hiding|import|in|inductive|infix|infixl|infixr|instance|let|macro|module|mutual|no-eta-equality|open|overlap|pattern|postulate|primitive|private|public|quote|quoteContext|quoteGoal|quoteTerm|record|renaming|rewrite|syntax|tactic|unquote|unquoteDecl|unquoteDef|using|variable|where|with)(?=$|[[:space:]\\(\\){}])"
    }
  ]
}