{"@context":"https://w3id.org/codemeta/3.0","@type":"SoftwareSourceCode","identifier":"pkg:hackage/MiniAgda","name":"MiniAgda","description":"MiniAgda is a tiny dependently-typed programming language in the style\nof Agda. It serves as a laboratory to test potential additions to the\nlanguage and type system of Agda. MiniAgda's termination checker is a\nfusion of sized types and size-change termination and supports\ncoinduction. Equality incorporates eta-expansion at record and\nsingleton types. Function arguments can be declared as static; such\narguments are discarded during equality checking and compilation.\nRecent features include bounded size quantification and destructor\npatterns for a more general handling of coinduction.","version":"0.2025.7.23","softwareVersion":"0.2025.7.23","license":"https://spdx.org/licenses/MIT","codeRepository":"https://github.com/andreasabel/miniagda","issueTracker":"https://github.com/andreasabel/miniagda/issues","url":"http://www.cse.chalmers.se/~abela/miniagda/","keywords":["dependent-types","library","mit","program","Propose Tags"],"programmingLanguage":{"@type":"ComputerLanguage","name":"Haskell"},"maintainer":[{"@type":"Person","name":"AndreasAbel"}],"author":[{"@type":"Person","name":"AndreasAbel"}],"copyrightHolder":[{"@type":"Person","name":"AndreasAbel"}],"dateCreated":"2014-01-09","dateModified":"2025-07-23","datePublished":"2025-07-23","copyrightYear":2014,"downloadUrl":"https://hackage.haskell.org/package/MiniAgda-0.2025.7.23/MiniAgda-0.2025.7.23.tar.gz","applicationCategory":"hackage","runtimePlatform":"hackage","developmentStatus":"active","sameAs":["https://hackage.haskell.org/package/MiniAgda"],"https://www.w3.org/ns/activitystreams#likes":115,"https://forgefed.org/ns#forks":4}