--- Day changed Wed Sep 13 2017
mckeankylejIs there a better way of getting this record into scope? http://lpaste.net/35839213/09 04:00
mckeankylejThe ugliness is at line 3913/09 04:01
glguyNot really, but you can knock about a few arrows: {F : Set} (f : Field F) (a b : F) -> let open Field f in (- a) · b ≡ - (a · b)13/09 05:30
mckeankylejman thats a shame idris' using notation would help here alot13/09 05:37
mckeankylejglguy: if I just work in the field of Q could I simplify it?13/09 05:40
tomjack_do you already know this? do you have only one thing to say about f? :) https://www.irccloud.com/pastebin/RJIInoLN/13/09 05:56
mckeankylejtomjack_: holy shit!!!! thanks and yea I only have one thing to say13/09 06:05
mckeankylejwow agda's module system is really powerful13/09 06:38

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