--- Day changed Tue Jan 24 2017
mpickeringWhere is subst defined in the stdlib?24/01 11:50
mpickeringand how can I find these things24/01 11:50
Eduard_Munteanumpickering, https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/PropositionalEquality/Core.agda24/01 12:04
Eduard_MunteanuUnfortunately we don't have a Hoogle for Agda.24/01 12:04
Saizan_M-. on subst in the emacs mode also works24/01 12:29
apostolisIs there a syntax to explictly annotate the type of a variable?24/01 15:09
apostolisSome times in a propositional equality, it is difficult for agda to infer the types of the values if they are expressions :  expression1 \== expression224/01 15:13
mietekapostolis: there’s a stdlib function, https://agda.github.io/agda-stdlib/Function.html#248124/01 15:13
apostolismietek : noce.24/01 15:15
apostolisnice24/01 15:15
SuprDewdI'm having trouble using mapM: http://lpaste.net/35159824/01 17:57
SuprDewdcan anyone see what I'm missing?24/01 17:57
SuprDewd(I mightt be missing a  >>= (return unit) at the end since this is not mapM_, but that doesn't seem to help.)24/01 18:05
{AS}SuprDewd: what's the error?24/01 18:05
{AS}I think you get List Unit back24/01 18:07
{AS}You basically want to ignore that 24/01 18:07
SuprDewd(ℕ → IO Unit) !=<24/01 18:07
SuprDewd(.Category.Monad.Indexed.RawIMonad (λ _ _₁ → _M_10)) of type Set24/01 18:07
SuprDewdwhen checking that the expression doit has type24/01 18:07
SuprDewd.Category.Monad.RawMonad _M_1024/01 18:07
{AS}SuprDewd: flip the arguments 24/01 18:07
SuprDewdI changed it to (mapM doit list) >>= (return unit)24/01 18:08
SuprDewdarguments to which function?24/01 18:08
{AS}Use mapM list doit24/01 18:08
SuprDewddoes that make sense? it still gives me an error24/01 18:09
SuprDewdthe type is mapM : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (List B)24/01 18:09
SuprDewdso I would expect the function to come first24/01 18:09
{AS}SuprDewd: I know now24/01 18:13
{AS}Have open RawMonad {{...}}24/01 18:13
pgiarrussoeverybody (and mietek): how hard is adding products to hereditary substitution for STLC? I seem to remember it is not hard but I’ve seen this discussed on IRC (here or in #dependent, not sure…)24/01 22:35
pgiarrussoaugur, gallais: ^^ or did you have a clue on hsubst for products?24/01 23:09
auguri cant see the relevant scrollback24/01 23:10

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