search

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

Maintain invariant that neutral types only have neutral elements #193

Open jonsterling opened 6 years ago

jonsterling commented 6 years ago

Right now, hcom,ghcom violate this invariant. We would need to add nghcom.

favonia commented 6 years ago

This will be closed by #270, right? @jonsterling

jonsterling commented 6 years ago

I hope so, I am not certain.