On Mon, Jul 7, 2014 at 6:45 PM, Geoffrey Irving <[email protected]> wrote: > On Mon, Jul 7, 2014 at 3:30 PM, Matt Oliveri <[email protected]> wrote: >> But maybe I'm misunderstanding you. > > I think so, since "checking in proofs" in this context means checking > them into a version control system (I was agreeing with shap).
Oh! Yes, that's very different. I didn't see that come up. I need to reread a lot of this thread now. > If > you're responding to specific language in a post it's better to reply > below the quoted paragraph, by the way. Sorry, I usually do that, but I thought for a short reply it'd be OK. It won't happen again. >> Anyway, I have an idea about how to avoid the limitations of a fixed >> "official" proof checker. It's what I've been thinking about since >> then. It's overkill though, given that BitC is just dabbling with >> dependent types. (Or at least that's my understanding.) > > I'd be very curious to hear it. Maybe another thread unless shap > thinks we've veered out of bitc territory? This one about grammar is > getting a bit long. I'll reply just to you until Shap wants to hear it. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
