Arnoud van der Leer

Yeah! Just enable switching between auto-fetching prices and fetching prices with a button, just like with snapshots. Also, currently, when new prices have been fetched, the change in net worth...

It seems that currently there is an emergent "standard" to have all identifiers written in `snake_case`. See, for example, #1814 , #1831 (, #1768 ). Would it be an idea...

I wrote two python scripts to maybe make this a bit easier. They utilize the `.glob` files that are generated on compilation: * One script that, given a directory, generates...

> Why bother with a wholesale renaming of identifiers? We'll get a reputation for making breaking changes, if we do that. I think there are good reasons to bring old...

And I know that we can probably not do this change overnight. I just hope that we can at least prepare such a change, finalize the list of substitutions, notify...

(See also [the corresponding discussion on the zulip](https://coq.zulipchat.com/#narrow/stream/256336-jsCoq/topic/How.20to.20create.20a.20version.20of.20jsCoq.20with.20more.20packages.3F/near/370447845))

@nmvdw This is resolved now, right?

I agree with Peter in this (although I don't know a lot about . The term "power" here is used in the same sense as "x to the power n...

@benediktahrens @nmvdw What do you think of this proposal? Do you think it is wise to keep using the name dagger category, or do you think another name is preferred?

Would it be an idea to add a note to the file, mentioning the (Dan's) objections?