Ali Caglayan

There is also the issue of `paths` which I haven't touched. Should we rename it to `Paths` or more correctly `Path`?

@mikeshulman Any thoughts on this?

@jdchristensen Can I get your thoughts on this also?

Rebased

Since everything will become a de Bruijn index behind the scenes, mangle names simply pokes all possible alpha conversions. This does end up changing goals as you have observed. I...

There is in fact a command line parameter `-mangle-names` which can be passed to coqc so that we only mangle on compilation. We could even do: ```coq Set Mangle Names...

So I've changed this line of the makefile: ``` $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq -arg -mangle-names -arg "_Please_do_not_rely_on_autogenerated_names_" ``` This means there will be no name mangling during interactive development,...

In fact it seems to be worse, it looks like before the option wasn't being exported before since I forgot to put a `Global`. Looks like we are relying on...

So here is a silly answer: the positives don't have a zero. I wrote the binary positives based off of the coq stdlib implementation. This allowed us to have an...

@jdchristensen Do you find working with binary positives difficult? There are some custom induction principles for doing case analysis on successors. However there is very little arithmetic for Pos (but...