--- Day changed Tue Feb 28 2017
wedifycould someone point me to an example. i would like to know how to index a list where i know all the keys exist, so i don't have to have a maybe type28/02 04:42
wedifyor some datastructure that does such28/02 04:42
wedifyok i figured out how to use the Any type28/02 04:59
wedifyso i think my question is a non-problem now28/02 04:59
wedifyit's "finished"!28/02 06:34
wedifynow to test it28/02 06:34
lpaste_wedify pasted “here's the interesting bit for those curious” at http://lpaste.net/35304428/02 06:35
wedifyi suppose to solve my problem i can have a constructor that returns a vector and takes a proof that all the keys are in the vector. then i just use vector operations28/02 06:50
wedifynow that i'm trying to prove things about games i realize just how many proofs are required. even just establishing that the initial board is not in check is hard28/02 07:00
wedifyaaaahhh! i've been working through a proof that the king is not in check in the initial board. i'm already at five hundred lines. i need to do something differently28/02 07:08
ezyang"sounds like you need some proof automation" 28/02 07:08
wedifyhow do i go about doing that?28/02 07:09
wedifyi will make everything implcit and see if agda can figure it out28/02 07:09
wedifyhmm looking around i see a paper on integrating waldmeister into agda. is there source somewhere? or does agda already have this?28/02 07:22
akr"Sweetscented bedstraw"?28/02 08:50
akrah http://www.waldmeister.org/28/02 08:51
jonsterlingDoes anyone on this channel work on the guts of Agda? I had a question about a feature...28/02 14:08
jonsterlingIn particular, is there a way to add "print statements" to the reflected TC monad? It would be so sweet to have a way to debug tactic scripts. 28/02 14:09
mietekMaybe Saizan28/02 14:56
{AS}wedify: I would probably split up the relations28/02 15:05
{AS}Like one that checks separate properties separately28/02 15:06
{AS}So CanMove(p, fromPos, toPos) = InPattern(p, fromPos, toPost) /\ NotInCheck(toPos) /\ ...28/02 15:07
{AS}etc.28/02 15:07
glguyjonsterling: you probably already figured out that you can "print" via the TC error mechanism28/02 15:09
glguybut if not, you can :) unfortunately it's fatal to the process28/02 15:10
{AS}wedify: Then you can describe the moves by https://en.wikipedia.org/wiki/Algebraic_notation_(chess), and the Agda program would check whether such a move script is valid :)28/02 15:10
{AS}So in essence you define that a play is a list of moves, with the invariants we talked about28/02 15:12
jonsterlingglguy: Yeah... I wanted something that wouldn't scuttle the process, since I'd like to print more than one thing  :). I guess I could hack up some kind of a monad that would let me run something in "printing mode", haha...28/02 15:13
stoopkidI'm getting an emacs error "File mode specification error: (file-error Searching for program No such file or directory agda)", anyone know how I might go about fixing this? 28/02 22:41
wedifystoopkid: is '~/.cabal/bin' in your PATH?28/02 23:20
stoopkidnope, doesn28/02 23:21
stoopkiddoesn't exist*. I'm on a Mac, that might be making things screwy28/02 23:21
stoopkidI managed to get it to work just now though by changing the agda2-program-name variable in agda2-mode.el to use the absolute file-path to the agda bin28/02 23:22

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