search

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

First draft at delta-nbe (doesn't work) #17

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

Tests in nbe-test all pass, but I get a strange error while certifying prelude. Probably a conceptual problem, I can't find any easy mistake