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

smalltt #476

Closed spitters closed 1 year ago

spitters commented 5 years ago

This is apparently very fast. Are any of the ideas useful in redtt? https://github.com/AndrasKovacs/smalltt

jonsterling commented 5 years ago

I am expecting that some of Andras's ideas will indeed be applicable :) I'm excited to study it.

favonia commented 1 year ago

Ideas are being explored in algaett.