Report or block andreasabel
Contact Support about this user's behavior.Report abuse
A prototypical dependently typed languages with sized types and variances
Formalizations of strong normalization proofs
Evaluation of typed terms in Agda using the Delay monad.
Prototypical type checker for Type Theory with Sized Natural Numbers
Stuff concerning sized types.
969 contributions in the last year
Created an issue in agda/agda that received 2 comments
Since very recently (just observing this behavior for the first time now), the emacs mode seems broken: postulate A : Set -- Comment postulate B : Set