--- Day changed Mon Jun 12 2017
Nik05mietek, yes sorry typo12/06 00:45
Nik05Now I also need to learn emacs...12/06 00:50
Nik05(Coq uses it too)12/06 00:50
lapinotNik05: funny, i'm starting this kind of things too, and i had the *exact* same feeling regarding coq tactics and the curry-howard isomorphism12/06 01:34
lapinotmietek et al: sorry for last night, i started some discussion and then i just went to sleep (totally exhausted), but i checked out some of the links (linear lisp..) you answered12/06 01:35
mieteklapinot: no worries12/06 06:16
Nik05Goodmorning12/06 08:02
Nik05I defined a pair "A × B = Σ A (λ _ → B)12/06 12:25
Nik05With type Set -> Set -> Set12/06 12:25
Nik05I have also create a const function from {A B : Set} -> A -> B -> A12/06 12:26
Nik05Why cant I define "A × B =  Σ A (const B)" ?12/06 12:28
Nik05oh I guess I need levels here12/06 12:33
Nik05cant just fix it with Set112/06 12:33
Nik05or i need to make a const1 function12/06 13:25
Nik05never thought about but predicates are jn Set112/06 13:28
comieteknot really12/06 13:30
comietekhttp://agda.github.io/agda-stdlib/Relation.Unary.html#54112/06 13:31
{AS}Nik05: you can write a universe polymorphic version of const12/06 13:37
{AS}const : \forall {\alpha \beta} {A : Set \alpha} {B : Set \beta} -> A -> B -> A12/06 13:37
Nik05comietek its not in Set1?12/06 13:46
Nik05but with that definition and \Sigma, which set is in Set1?12/06 13:47
comietekNik05: if you insist on doing this stuff, you should just bite the bullet and learn to use levels12/06 13:52
comietekNik05: my simple prelude may be helpful; https://gist.github.com/mietek/a0e2a3998f21520e9230222a79d882c412/06 13:53
comietekit's very specific for the kind of stuff that I do though12/06 13:53
Nik05oke12/06 13:55
Nik05thanks for the help12/06 13:55
Nik05thats almost what i got except for the levels12/06 14:02
Nik05I guess using levels isnt that much of a problem. I do find it really verbose and makes types harder to read12/06 14:02
comietekyes12/06 14:07
comietekhowever, this isn't really an issue once you get to more interesting things12/06 14:08
comietekit's the lowest-level building blocks which really should be level-polymorphic, so that they won't get in the way12/06 14:08
Nik05Oke thank yoy12/06 14:10
Nik05is that the definition of Nat you use? is the one with reflexivity and step too hard to use?12/06 14:12
Nik05What is the location to put your local files? I found jnformation on how to create libraries etc but they all talk about default system directory. 12/06 23:40
Nik05or do you just choose a location and the module names say which directory to use relative to your current file?12/06 23:41

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