repo ""
commit ""
license ""

grammar {
    id "agda"
    name "Agda"
    tag "code"
    tier 4
    has-scanner #true
    tests-cursed #true // Unicode in highlights.scm breaks on Windows

    inventor "Ulf Norell"
    year 2007
    description "A dependently typed functional programming language and proof assistant."
    link "https://en.wikipedia.org/wiki/Agda_(programming_language)"
    trivia "Agda's name comes from a Swedish song about a woman named Agda who had a hen that laid eggs containing the words of the song."

    sample {
        path "samples/List.agda"
        description "Agda standard library List module with dependent types and pattern matching."
        link "https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Base.agda"
        license "MIT"
    }
}
