rephrase: more 'conventional' phrasing of DTFP?

agda · Sep 3, 2024 · ed5227f · ed5227f
1 parent 28f3f71
commit ed5227f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/paper/paper.md b/paper/paper.md
@@ -42,7 +42,7 @@ bibliography: paper.bib
 
 # Summary
 
-Agda[@norell2009dependently] is a functional, dependently-typed language that serves both as a traditional programming language and as an interactive theorem prover (ITP).
+Agda[@norell2009dependently] is a dependently-typed functional language that serves both as a traditional programming language and as an interactive theorem prover (ITP).
 This paper introduces the Agda standard library, which offers many of the fundamental definitions and results necessary for users to quickly begin developing Agda programs and proofs.
 Unlike the standard libraries of traditional programming languages, the Agda standard library not only provides standard utilities and data structures, but also a substantial portion of the basic mathematics essential for proving the correctness of programs.