--- Day changed Fri Aug 25 2017
WilliamHamiltona little syntax question: in the standard library https://agda.github.io/agda-stdlib/Data.List.Base.html there is a function _∷ʳ_ to append elements to the end of the list25/08 13:36
WilliamHamiltonhow does one actually write that `r` in the emacs frontend? I wasn't able to find any definition in https://github.com/jwiegley/agda-mode/blob/master/agda-input.el25/08 13:37
WilliamHamilton(I would have expected something like `\^r`, but only `\^i` is defined25/08 13:37
mietekWilliamHamilton: \^r425/08 13:41
mietekor, \^r C-f C-f C-f C-space25/08 13:41
mietekand it remembers the last choice, so next time it should be \^r25/08 13:41
WilliamHamiltonthanks (hi! I studied and I'm implementing the last chapter of verified programming)25/08 13:41
mietekcool25/08 13:41
mietekwhenever you have a unicode character you don’t know how to type, you can hit25/08 13:42
WilliamHamiltonthe plan is to construct a term aware version immediately after25/08 13:42
WilliamHamiltonperfect, I will! :)25/08 13:42
mietekC-u C-x =25/08 13:42
WilliamHamiltonoooh25/08 13:42
WilliamHamiltonno, can you tell me the name of the command?25/08 13:43
mietekhttp://agda.readthedocs.io/en/latest/tools/emacs-mode.html#ok-but-how-can-i-find-out-what-to-type-to-get-the-character25/08 13:43
WilliamHamiltonoh, describe-char25/08 13:43
WilliamHamiltoncool!25/08 13:43
WilliamHamiltonwhat's the default fixity of an operator? What's the fixity of _->_?25/08 15:09
WilliamHamiltonhow do I discover fixities? Is there a :info command saying that like in haskell?25/08 15:09
WilliamHamilton(20 for an operator, ok, but how do I discover the one for _->_?25/08 15:10
dolioI think arrow is lower than anything you cna define yourself.25/08 15:33
dolioIt's not really an operator (last I checked).25/08 15:33
mieteknote you can have negative fixities25/08 18:09
mietekAFAIR25/08 18:09
dolioYeah, I think so. I don't know if those go lower than function arrow, though.25/08 18:29
mietekme neither25/08 18:31
WilliamHamiltonthanks dolio25/08 19:24
WilliamHamiltonalso, I have another question on agda usage: to have a concrete example I'll refer to this http://www.speleologic.net/PPDP-2014-tutorial/KripkeCompleteness.agda but the question is not about the particular content25/08 19:31
WilliamHamiltongiven the definition of Γ ⊢ A in that file, at a certain point I want to pattern match on it25/08 19:32
WilliamHamiltonso, keeping the soundness theorem as an example25/08 19:32
WilliamHamilton    soundness : ∀ {Γ A} → Γ ⊢ A → {w : K} → w ⊪ Γ → w ⊩ A25/08 19:32
WilliamHamilton    soundness hyp (w⊪A , w⊪Γ') = {!!}25/08 19:33
WilliamHamiltonis the first clause; now, if I inspect the goal and the context I can see that the matching hyp has forced `Γ ⊢ A` to be of the form `A :: Γ' ⊢ A` for suitable Γ'25/08 19:34
WilliamHamiltonand the autogenerated name for `Γ'` is `.Γ` which as I just learned is referred to as a `dot pattern`25/08 19:35
mieteknot really; Agda unfortunately overloads the meaning of .25/08 19:36
mietek`.Γ` simply means here that there’s an implicit variable named `Γ` 25/08 19:36
WilliamHamiltonafter this preamble, the question: is there a way in which I can properly name that implicit variable?25/08 19:36
mietekyou can bind it by putting in `{Γ}` somewhere to the left of the `=`25/08 19:36
mietekor `{Γ = your-name-for-Γ}`25/08 19:37
mietekyou can see an example of Ilik doing that in `⊪-≥`25/08 19:37
mietekand in the last case for `soundness`25/08 19:37
mietek a dot-pattern is a pattern match that is forced by another pattern match25/08 19:38
mieteksomething a bit different25/08 19:38
WilliamHamiltonbut that will name the actual occurrence of Γ: if I write25/08 19:38
WilliamHamilton    soundness {Γ} hyp (w⊪A , w⊪Γ') = {!!}25/08 19:38
WilliamHamiltonthis will actually bring in scope Γ, but do nothing to rename the .Γ, that will remain there25/08 19:38
WilliamHamiltonI also tried something along the lines of25/08 19:39
WilliamHamilton     soundness {Γ@(A∷Γ′)} hyp w⊪Γ@(w⊪A , w⊪Γ') = {!!}25/08 19:39
mietekthat’s not the right place25/08 19:39
WilliamHamiltonok, what's the right place and how can I discover it by myself25/08 19:39
WilliamHamilton?25/08 19:39
mietek`soundness (hyp {Γ}) ρ`25/08 19:39
WilliamHamiltonright, now I feel dumb :D25/08 19:40
mietekit is a bit unclear25/08 19:40
mietekBTW, why do you insist on `(w⊪A , w⊪Γ')`?25/08 19:40
WilliamHamiltonbecause that's the meaning of the two pieces: one is a proof that w entails A, and the other the rest25/08 19:41
mietek`soundness hyp ρ = proj₁ ρ` also works25/08 19:41
WilliamHamiltonhaving good names helps me to see the proofs earlier (maybe it's just the inexperience)25/08 19:41
mietekfair enough25/08 19:41
mietekjust wanted to highlight that not in all cases we will know that `ρ` is non-empty25/08 19:41
WilliamHamiltonoh yes, right, I was in search for a mechanism to more readily express: when I have this pattern match, this generic argument becomes this one; for example25/08 19:43
WilliamHamilton    soundness {Γ@(A∷Γ′)} (hyp {Γ'}) w⊪Γ@(w⊪A , w⊪Γ') = {!!}25/08 19:44
WilliamHamiltonwhile is certainly overkill for this simple example, expresses neatly, in my opinion, how25/08 19:45
WilliamHamiltonwhat I called Γ before is (A∷Γ′) now25/08 19:45
WilliamHamiltonetc25/08 19:45
WilliamHamiltonbecause I don't like that a moment before I called Γ something, and now there is a .Γ that it's relatively unrelated, and no place where their relation is expressed25/08 19:47
WilliamHamiltonhowever, I will report back when I'll need no more this aids :D25/08 19:47
mietekI recognise the dilemma25/08 19:59
kclancyI'm getting a subtyping error that I do not understand when I try to typecheck Reduction.agda in this repo: https://github.com/kevinclancy/model225/08 21:27
kclancyMaybe not a subtyping error, actually. Just some typing error. I did not expect this error to happen due to the subtyping rule for sized types that says D i <: D inf.25/08 21:33
kclancyWhere i is some size.25/08 21:33

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