From 6f4e1ffbaa930d6d91e2e3b8dfb4762d9f68c14d Mon Sep 17 00:00:00 2001 From: Ben Date: Wed, 6 Jan 2016 14:06:17 -0500 Subject: [PATCH] Fix typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 29c99061..e2c96b66 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Ideas - Notations should be hidden by modules that are explicitly opened. - This avoids clashes between precedence. - TB: Actually, this does not completely avoid clashes, if we have to open two modules at the same time (for instance, I often need to open Equality, to get dependent destruction, which conflicts with the rest of my development) - - TB: I like the idea of having to prefix operations by the name of the module (e.g., DList.fold, DList.map, DList.T), and yet to benefit from the support of notations, without opening this module. I implement that by having a module DList that contains the operations, inside the file DList. The notations leave in the file DList, and I do Require Import DList everywhere... + - TB: I like the idea of having to prefix operations by the name of the module (e.g., DList.fold, DList.map, DList.T), and yet to benefit from the support of notations, without opening this module. I implement that by having a module DList that contains the operations, inside the file DList. The notations live in the file DList, and I do Require Import DList everywhere... - Avoid the use of the 'core' hint database. - Avoid the use of dependent functions, e.g. dependendent decidable equality, in favor of their boolen counter-parts. Use type-classes to expose the proofs.