--- Day changed Sat Aug 19 2017
apostolisHello, I am searching for exercises on cubical : HITs , univalence , quotient types.19/08 09:22
apostolisI am using mortbergs' cubicaltt and have read the lectures there.19/08 09:23
apostolisCubicaltt has many examples, but I would prefer if I was pointed to simple things first.19/08 09:25
madgenHello! The newest Homebrew version seems to break Vim support (goal is never loaded), I searched through homebrew, agda-vim, and agda repo issues, but couldn't find anything. Any chance this is common knowledge?19/08 23:36
madgen2.5.3-alpha1 that is19/08 23:36
mietekmadgen: sorry, that sounds like a niche of a niche of a niche19/08 23:38
mietekmadgen: Vim, as in, emacs-Vim compatibility?19/08 23:39
madgenVim as in agda --vim through github.com/derekelkins/agda-vim19/08 23:40
mietekoh dear19/08 23:40
mietek:)19/08 23:40
mietekI actually do use the Homebrew formula for Agda19/08 23:41
mietekbut I don’t think that’s related19/08 23:41
mietekit sounds like agda-vim may need to be updated for 2.5.3?19/08 23:41
madgenMaybe! Thought I would ask around before I open an issue.19/08 23:42
madgenmietek: actually building HEAD right now to see if the problem goes away, so I should have a definitive answer in maybe three four days.19/08 23:42
mietek:)19/08 23:43
madgenThe CHANGELOG on Agda repo doesn't mention an API change either.19/08 23:44
madgenIt persists in 2.619/08 23:57

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!