--- Day changed Mon Feb 12 2018
lapinothi12/02 00:09
lapinoti'm starting to want to do some stuff in agda now that i lurk in the documentation and fiddle with some tutorials since a while...12/02 00:10
lapinotwould be coq's small-scale reflection of any use in agda? i mean the `reflect (P: Set) : Bool -> Set` predicate reflecting boolean logic and propositional logic12/02 00:12
lapinotas i only have base knowledge of agda and ssreflect i have trouble understanding the underlying questions but one thing that appealed to me is that ssreflect is said to help to control how computation is done12/02 00:39
lapinotas agda is much more oriented towards computation than coq i would be interested to hear what people knowing ssreflect and agda a bit more have to say about this12/02 00:40
{AS}lapinot: usually you would use decision procedures in Agda12/02 07:34
{AS}E.g., Dec P 12/02 07:34
{AS}augur: Did you use agda-mode setup ? 12/02 07:35
augur{AS}: yeah, that didn't do anything :(12/02 08:26
{AS}Hmm 12/02 08:26
{AS}augur: How did you install agda-mode?12/02 08:26
{AS}Btw, I use Emacs on OS X, it is usually more stable than Aquamacs12/02 08:27
auguri think it came w/ the nightly of agda through stack12/02 08:27
auguremacs w/ iterm doesnt work completely12/02 08:28
auguragdamode works there but not all key combos12/02 08:28
{AS}I meant https://emacsformacosx.com/ :)12/02 08:28
{AS}You can also install it via Homebrew12/02 08:29
{AS}Aquamacs is known to have issues with some packages12/02 08:32
{AS}I can't recall if Agda was one12/02 08:32
{AS}augur: ^12/02 08:32
augurhmm ok12/02 09:36
lapinot{AS}: oh indeed, Dec looks a lot like reflect, i'll look into that12/02 14:02
lapinotactually i didn't realize reflect was about decidable things12/02 14:03

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