From 58893fc3f77480f1ebd377c1d81c5dbb7b4681f0 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 22 Mar 2016 15:29:54 +0100 Subject: [PATCH] TODO --- prelude/functions.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prelude/functions.v b/prelude/functions.v index 1ae5080e7..935d1b448 100644 --- a/prelude/functions.v +++ b/prelude/functions.v @@ -8,7 +8,7 @@ Section definitions. λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b. End definitions. -(* For now, we only have the properties here that do not need a notion +(* TODO: For now, we only have the properties here that do not need a notion of equality of functions. *) Section functions. -- GitLab