Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Browse files


Some discussion about notations
  • Loading branch information...
1 parent 60c4b96 commit ee859a875b4a5a083b8e81e340637385a5e3ed4c @braibant braibant committed
Showing with 3 additions and 1 deletion.
  1. +3 −1
@@ -9,7 +9,9 @@ Ideas
- Avoid functors in favor of type classes since type classes are more flexible
b/c they are first-class.
- Notations should be hidden by modules that are explicitly opened.
- - This avoids clashes between precedence.
+ - 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.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...
- 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.

0 comments on commit ee859a8

Please sign in to comment.
Something went wrong with that request. Please try again.