From c621331cc141a965dcf2c1f2a9a62934e0703762 Mon Sep 17 00:00:00 2001 From: thyecust Date: Sun, 16 Oct 2022 16:10:58 +0800 Subject: [PATCH] fix typo in strict-positivity --- src/strict-positivity.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/strict-positivity.md b/src/strict-positivity.md index 9855532..fb4f141 100644 --- a/src/strict-positivity.md +++ b/src/strict-positivity.md @@ -10,7 +10,7 @@ Inductive bad := r (c : bad -> nat). ```agda -- rejected by Agda data Bad : Set where - r : (Bad → ℕ) → Curry + r : (Bad → ℕ) → Bad ``` Here, the type `bad` is defined recursively as consisting of a @@ -157,4 +157,4 @@ three are necessary: [^abel]: Section 7.1 of [A Semantic Analysis of Structural Recursion](http://www.cs.cmu.edu/~abel/publications.html), Andreas Abel (1999) -[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006) \ No newline at end of file +[^blanqui]: [Inductive types in the Calculus of Algebraic Constructions](https://arxiv.org/abs/cs/0610070), Frédéric Blanqui (2006)