RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

Factor out Favonia Namespace code into library #488

Open jonsterling opened 4 years ago

jonsterling commented 4 years ago

For now, just a local library in this repository.

ivoysey commented 4 years ago

Sounds good. For updating the version, I defaulted to making a fork on my own account and doing a PR from that without actually asking if that's the right thing to do. Is that a reasonable process for you? @cangiuli suggested that it might be better if I made a branch on this repo and a PR from that to master, so that it'd be easier for other folks to work on what I'm working on.

jonsterling commented 4 years ago

Good question! We usually work on branches in the main repo rather than forks.

ivoysey commented 4 years ago

Gotcha; I'll use that style from now on, then.