search

fpvandoorn / lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)
Apache License 2.0
0 stars 0 forks source link

formalize dependent smash #8

Closed fpvandoorn closed 6 years ago

fpvandoorn commented 6 years ago

https://github.com/cmu-phil/Spectral/blob/master/homotopy/dsmash.hlean