vorgang vorgang wedify --- Day changed Mon Mar 27 2017 wedify: thanks, it was using /usr/bin/agda, not the cabal version. Deleted that, it works now. There's seems to be no stdlib though.... 27/03 04:11 Does the cabal package "Agda" also include stdlib? 27/03 05:38 vorgang: no it does not 27/03 08:58 easy to set it up though 27/03 09:00 mietek: it's in "i have to document it" status, so actually more users would be nice 27/03 10:13 mietek: it's merged in master 27/03 10:13 Saizan: cool. 27/03 10:13 {AS}: ^^ 27/03 10:13 ah cool 27/03 10:13 I’m having trouble locating Catarina Coquand’s webpage… 27/03 10:14 Anyone? 27/03 10:15 mietek: link 27/03 10:16 {AS}: I can’t find a link; that’s the thing 27/03 10:17 ah 27/03 10:17 I think I thought you meant accessing 27/03 10:17 That’s very self-reflective of you 27/03 10:18 mietek why do you need her webpage? 27/03 10:21 I want to ask if she still has the full Alf code accompanying her 2002 paper 27/03 10:21 I can't find it 27/03 10:21 Ah 27/03 10:21 you can just use the registry of Chalmers no? 27/03 10:21 http://www.hh.se/omwebbplatsen/sokpawebbplatsen/personalkatalog.2637.html?url=-1708965309%2Fl9%2Fhhstaff%2Fen%2Fdetail.lasso%3Fdo%3Dstart%26groupmember%3D35AA3CED-44BF-4833-A72E-B8AA19AF7850&sv.url=12.2a98b8e2153dde2b50b95569 27/03 10:21 This seems to be current 27/03 10:22 yeah 27/03 10:24 I see 27/03 11:53 err, wrong channel 27/03 11:53 wedify: but how? I can't find a cabal package for Agda stdlib 27/03 18:27 The Agda std-lib isn't a Haskell library, it's an Agda library; there's no cabal package for it 27/03 18:29 vorgang: Here's how I've got it setup : http://lpaste.net/5211928558699544576 27/03 18:34 Do you run Agda from the git repo? I tried updating everything (library and binary) the other day, but the compiler didn't like something in the library. 27/03 18:37 I do, but I think it has tags to get particular version 27/03 18:40 I installed Agda from hackage, so maybe it's too old. 27/03 18:40 Yeah, you might have to roll back to an older tag for hackage 27/03 18:41 I appear to have "Agda version 2.5.2" and agda-stdlib commit a79f1fb7d78d4f5e042dcf553f8156ed85a146be specifically 27/03 18:41 glguy: So Agda knows about ~/.agda/libraries and ~/.agda/defaults ? 27/03 20:05 glguy: it kind of works now... at least I get a different error 27/03 20:26 glguy: did you also compile agda-stdlib, or just pull the repo? 27/03 20:28 I've found myself needing a universe-polymorphic bottom type. Is this reasonable in any way shape or form? Or should I reevaluate my terrible decisions? 27/03 20:37 sleffy: ⊥ itself, or ⊥-elim? 27/03 20:42 mietek, \bot itself. 27/03 20:42 can you give an example of how this happens? 27/03 20:42 I have a feeling this is due to my naivete 27/03 20:42 I could imagine some places where it might come up. 27/03 20:43 mietek: https://pastebin.com/raw/450TBKHZ 27/03 20:44 I have cases where I have a Maybe A where A is not in Set 0. In that case, NoConfusion-Maybe has to put out an equality which is in Set l, where l is whatever level A is in 27/03 20:45 I’m quite confused 27/03 20:45 Yeah, that's not a big surprise. I don't really know what I'm doing 27/03 20:45 What I wanted to do was be able to take any equality of the form just x = nothing or nothing = just x, and produce bottom 27/03 20:45 are you trying to write a decidable equality? 27/03 20:45 No 27/03 20:45 I'm trying to prove that a partial function always produces just x when given a particular sort of proof on its inputs 27/03 20:46 In the process, I end up with a lot of inequalities of the form just x = nothing or nothing = just x 27/03 20:46 well : ∀ {ℓ} {X : Set ℓ} {x : X} → just x ≡ nothing → ⊥ 27/03 20:46 well () 27/03 20:46 So I wanted a tool to better deal with discharging them 27/03 20:47 I saw someone's NoConfusion implementation for I forget what type on the internet and then tried to imitate it :P 27/03 20:47 mietek, that's what I was originally going to do but I also end up with the other way around, and I was hoping to use the same lemma for both 27/03 20:47 llew : ∀ {ℓ} {X : Set ℓ} {x : X} → nothing ≡ just x → ⊥ 27/03 20:48 llew = well ∘ sym 27/03 20:48 Well, I'll run with that for now then. As an aside, how do you type the cursive l? 27/03 20:49 \ell 27/03 20:49 thx :) 27/03 20:49 welcome 27/03 20:49 also, c-U c-X = should tell you how to type any character you have highlighted in emacs 27/03 20:50 look for the 'to input:' line 27/03 20:50 That's really useful! Thanks again. 27/03 20:51 mietek, as an aside: on the well and llew definitions, Agda can't seem to infer the implicits on the just x ≡ nothing. I get a lot of "failed to solve constraints" errors. 27/03 20:57 If I rewrite the type signature to well : ∀ {ℓ} {X : Set ℓ} {x : X} → just x ⟨ _≡_ {ℓ} {Maybe X} ⟩ nothing → ⊥, then it works out, but it's a bit ugly. Is there a better way to give Agda the missing info? 27/03 20:57 try Maybe.just 27/03 20:57 the problem is name overloading in the stdlib 27/03 20:57 I use my own micro-prelude nowadays 27/03 20:57 oh, huh. That did the trick. Thanks again! 27/03 20:58 there are simply multiple just constructors in Data.Maybe 27/03 21:00 which is a bit weird 27/03 21:00 vorgang: I think I just pulled the repo. There might be elements that need to be compiled for uses I haven't tried 27/03 21:02 the Agda docs say that old-style coinduction with ∞ is inconsistent, but Google is not helping me find a counterexample. anyone know off the top of their heads? 27/03 22:21 christiansen: https://github.com/agda/agda/issues/1209 maybe ? 27/03 22:27 christiansen: https://github.com/agda/agda/issues/1209#issuecomment-129029487 <- sorry 27/03 22:27 {AS}: thanks 27/03 22:28 np 27/03 22:28 If you are trying to do your own coinduction I can recommend guarded recursive types :) 27/03 22:29 {AS}: I'm hunting Idris bugs, and old/fixed/wontfixed Agda bugs are a good source 27/03 22:29 best to learn from those who have come before :) 27/03 22:29 christiansen: Ah cool 27/03 22:29 I can still recommend guarded recursive types, but I guess we would need someone to implement them 27/03 22:29 you mean like the ones Rasmus & the Aarhus folks work on, right? 27/03 22:30 Yeah 27/03 22:31 You would probably also need cubical (AFAIR) to get equality working rightly 27/03 22:31 so I guess maybe after 1.0 27/03 22:32 OTT should work as well, I'd think - the key is getting canonicity + the right prop. eq. for codata, right? 27/03 22:32 christiansen: Hmm, yeah. It's because codata equality should be extensional 27/03 22:33 so if you care more about UIP than Path induction then OTT should work 27/03 22:33 * {AS} just wanted an excuse to get cubical into Idris :) 27/03 22:35 {AS}: K is baked in pretty solidly - it'd be a lot of work. I think Cubical Agda will be ready for play much sooner! 27/03 22:35 I was recently told that cubical Agda is ready :) 27/03 22:36 oh, great news! 27/03 22:37 * christiansen is behind on things 27/03 22:37 Yes, i've heard it basically works except for "with expressions"! Haven't gotten around to playing with it yet 27/03 23:16 Just finished up jrw's patch to support hypothetical judgments in user-level theorem declarations! 27/03 23:56 https://usercontent.irccloud-cdn.com/file/X3Zlc7mk/Screen%20Shot%202017-03-27%20at%206.55.11%20PM.png 27/03 23:57 This is the first step, I suppose, toward supporting MetaPRL-style sequent schemata. 27/03 23:57 Super excited about this. 27/03 23:57 Oops, I put this in the wrong channel. Sorry about that! 27/03 23:57