Where communities thrive

Join over 1.5M+ people
Join over 100K+ communities
Free without limits
Create your own community

Explore more communities

oeed/Silica

The next generation ComputerCraft GUI Framework

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

notpatrickadams forked
notpatrickadams/Silica
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

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)