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

Log levels for output hygiene #225

Open jonsterling opened 6 years ago

jonsterling commented 6 years ago

Ideally, nothing should be emitted that the user doesn't ask for.