Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Sep 19 2020 01:40

    oeed on develop

    Changed to MIT license (compare)

  • Feb 26 2020 21:37
    jmc529 starred oeed/Silica
  • Feb 23 2020 02:10
    xvxx starred oeed/Silica
  • Nov 05 2019 07:48
    jsgrant starred oeed/Silica
  • Oct 14 2019 01:32
  • Jun 28 2019 18:20
    adamc295 starred oeed/Silica
  • Mar 03 2019 01:37
    ardera commented #26
  • Feb 16 2019 02:37

    oeed on develop

    Update README.md (compare)

  • Feb 16 2019 02:34
    oeed closed #25
  • Feb 16 2019 02:34
    oeed commented #25
  • Feb 15 2019 22:33
    Lemmmy starred oeed/Silica
  • Feb 15 2019 15:29
    SquidDev commented #26
  • Feb 15 2019 14:55
    exerro closed #26
  • Feb 15 2019 14:55
    exerro commented #26
  • Feb 15 2019 14:36
    exerro commented #25
  • Feb 15 2019 14:26
    jojomoore2007 commented #26
  • Feb 15 2019 14:15
    jojomoore2007 commented #26
  • Feb 15 2019 14:14
    jojomoore2007 opened #26
  • Feb 15 2019 14:01
    jojomoore2007 opened #25
  • Feb 07 2019 23:03
    oeed closed #24
hydraz
@plt-hokusai
maybe we should have an amulet irc
Jonathan Coates
@SquidDev
Because the #urn one went so well :)
hydraz
@plt-hokusai
:p
Drew
@CoderPuppy
Have either of you looked at some of the new fancy type theories? Cubical or Quantitative?
Jonathan Coates
@SquidDev
I know Cubical exists, because the Agda people won't shut up about it. That's about the extend of my knowledge - I know hydraz has done more work on this.
hydraz
@plt-hokusai
i've played with cubical agda and read the hott book
i have a wip qtt checker but it is very wip
Jonathan Coates
@SquidDev
Is QTT the one Idris 2 uses?
Drew
@CoderPuppy
Yep
hydraz
@plt-hokusai
yep
Drew
@CoderPuppy
combining linear and dependent types
Jonathan Coates
@SquidDev
Yeah, I really should have remembered this...
Drew
@CoderPuppy
One thing about it that seems interesting is that I think it allows dropping the parametricity of Π(A : Type).
hydraz
@plt-hokusai
i mean, you can already do that with Typeable
or in a dependently typed language, codes for types
Drew
@CoderPuppy
so it might allow typed tactics (a la VeriML) directly in the language
hydraz
@plt-hokusai
i don't like matching on Type
i think matching is for inductive families only and Type is not an inductive family
Drew
@CoderPuppy
I actually found an oddity with that, Agda doesn't support matching on types but they used to make type constructors injective which is similar
they stopped that because someone found a contradiction, but I think that's just because positivity checking wasn't applied to type constructors (because you can't match on them)
Benedict Allen
@exerro
Woah, actually conversation on gitter
InternetUnexplorer
@InternetUnexplorer
Oh hey some activity
I seem to have missed it by a bit, but hello
João Victor
@jv110
hello
João Victor
@jv110
where else can I see you?
Andrew Kvapil
@viluon
Can't wait for the Silica release
@oeed has been working on it for so long, it has to be epic by now
João Victor
@jv110
oof
Jonathan Coates
@SquidDev
What on earth
pjals
@pjals:matrix.org
[m]
is silica gonna be continued?
Benedict Allen
@exerro
of course
Jonathan Coates
@SquidDev
doubt
Huh, I'd forgotten gitter was bridged to matrix now.
pjals
@pjals:matrix.org
[m]
ah, people actually are alive in this channel
Jonathan Coates
@SquidDev
To some extent, sure.
It's off screen on my channel list, so I never see it.
pjals (Daniel)
@pjals:matrix.org
[m]
hah
Benedict Allen
@exerro
Matrix seems neat
And yeah I just got an email and checked
pjals (Daniel)
@pjals:matrix.org
[m]
since i have no other computercraft related channels here, ill dump this here
Andrew Kvapil
@viluon
if it isn't (wasn't) @pjals:matrix.org! Long time no see
Dušan Havlík
@RatcheT2497_twitter
oh hey activity
wow i haven't been here in a while
how's things?
Jonathan Coates
@SquidDev
Huh, I didn't see this earlier.