--- Day changed Sun Jun 18 2017
Nik05Was trying to implement find from page 25 of DTPiA by Norell and Chapman, but then with P : A -> Set and not from A -> Bool18/06 14:06
Nik05Started out with some proofs tried a C-c C-a and there I got two full lines that proved it...18/06 14:07
Nik05Guess I understand it18/06 14:28
Nik05Can I get 'Compute normal form' to not print underlying definitions?18/06 14:35
Nik05.Agda.Builtin.List.List.:: to just print ::?18/06 14:35
mietekNik05: import Agda.Builtin.List ?18/06 15:22
mietekopen import18/06 15:22
mietekI would call that the module prefix18/06 15:22
mietekor path18/06 15:23
Nik05I used open import Data.List18/06 15:24
Nik05So how do I fold (Coq) this module prefixes?18/06 15:24
mietekdid you try what I said?18/06 15:24
Nik05oh thank you18/06 15:26
mietekhere we run into the stdlib design again18/06 15:26
Nik05should I import or open import Agda.Builtin.List?18/06 15:31
mietekit is the open that folds the prefix18/06 15:31
mieteksame applies to modules you define within the file18/06 15:32
mietekalso, modules that are implicitly defined by defining a record18/06 15:32
Nik05it still unfold the definition here18/06 15:33
mietekcan you paste your code?18/06 15:34
mietekhttp://gist.github.com/ works well18/06 15:34
Nik05Oh I fixed something by making a smaller paste...18/06 15:36
Nik05I had some code in an anonymous module18/06 15:36
mietek:)18/06 15:37
mietekthis happens often18/06 15:37
Nik05thank you mietek 18/06 15:38
Nik05mietek how would i also fold the definition in an anonymous module?18/06 15:45
mietekan anonymous module is automatically opened18/06 15:47
TanebSo, I'm trying to encode a pile of category theory in Agda18/06 19:57
TanebAnd to prove the category laws hold for functor categories, I need a notion of equality for functors18/06 19:58
TanebWhich is... more complicated than I'd like18/06 19:58
Nik05nice emacsOS crashes 18/06 20:49
Nik05Taneb I read some basic Category Theory by Bartosz. Do you maybe care to show some implementation?18/06 20:49
TanebNik05, very much a work in process but http://lpaste.net/35633218/06 21:05
Nik05thank you Taneb 18/06 21:16
Nik05And then the Agda tutorial talks about categories... Dont get this at all :P18/06 21:29
{AS}Taneb: Small style suggestion, but you may want to consider factoring out the proofs from the construction of records :)18/06 21:58
Taneb{AS}, how do you mean?18/06 21:59
{AS}like http://lpaste.net/356332#line8518/06 21:59
{AS}it may be easier to read if you had o-comm outside18/06 22:00
TanebI see what you mean, but that means having to have a separate top-level definition18/06 22:00
{AS}so the record constructor only delegates to function18/06 22:00
{AS}Yeah, it requires a bit more code, but I think it is nicer to read :)18/06 22:01
{AS}I think you may use a private module or something like that18/06 22:01
TanebYeah, that's a thought18/06 22:02
Nik05Does anyone have more emacs scripts I can use with agda? ex. with generation18/06 22:14

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