← Feed @ice1000@types.pl Post #3183683 2026-01-26 21:44 UTC @jesper In definitional proof-irrelevance without K, how did you setup this beautiful Rocq code syntax highlighting? Replies (0) No replies.