The Nineteenth Byte

« first day (5077 days earlier) ← previous day next day → last day (61 days later) »

Ginger

00:33

I lied :3

need to figure out why it's spamming messages in rooms that don't need to be antifrozen

rydwolf

01:07

I am considering buying a ruggedized laptop

rydwolf

01:20

Two hot-swappable batteries seems like such a W feature

and having 5G cell service on a laptop seems like something that'd be really handy whenever you need it

only problem is $2200 lmao

Ginger

01:36

lmao

amazing

rydwolf

I figured my friends from CMU would be confused but no they got the appeal instantly and now we're all just thirsting over this laptop together

lyxal

I didn't need to read that first one today

Anyone got a spare time machine? :p

Ginger

01:53

@Ginger I was treating a value in days as a value in milliseconds

rydwolf

IMO statically typed languages should have a way to specify the units of a numeric value

1 hour later…

user

03:13

I once had to contribute to a project that made use of a C++ library that uses templates to specify and check units

I soon found myself using it to calculate the speed I would need to reach, in kmph, to kill myself on impact upon jumping off a building

att

u ok?

1 hour later…

emanresu A

04:18

today I learned that SE has keyboard shortcuts

Redz

what.

WHAT.

my life has gained happiness

lyxal

@emanresuA you mean you've never accidentally pressed r before?

Or whatever key brings up the inbox

Because it's like not actually something you use very often

Over the last 4 or so years I've never actually needed keyboard shortcuts lol

Evidenced by the fact that despite knowing about them, I never use them

emanresu A

04:59

you do have to explicitly turn them on in settings

2 hours later…

att

06:51

@lyxal c is the one for me

i think

(tried a bunch of random keys and this was the first one that looked about right)

Neil

where is the list of shortcuts documented?

2 hours later…

Rosario

08:43

@l4m2 for me your = is <-> ; there was i time where i wrote all logic axioms and math axioms

possible symbols without a meaning

l4m2

09:06

@Rosario If (f->g) and (g->f) both provable, then f=(f->g)->(g->f)->f=(f->g)->(g->f)->g=g, this is proven not axiom

CMC Input /^(b*|#*)[A-G]$/, output an equal note with /^b+$/ig. E.g. C => bbbbbbbbbbbB

Rosario

09:27

@l4m2 if we can write "f->g" and "g->f" or in equilvalent way "f->g" and "g->f" are followed from the axioms, than we can write too "(f->g) and (g->f)" and "f<->g" not "f=g"

followed form axiom = derivati dagli assiomi, in pratica possiamo scrivere nel foglio di carta tutti gli insiemi di lettere o stringhe ricavate dagli assiomi

i don't understand f=(f->g)->(g->f)->f=(f->g)->(g->f)->g=g because = for me is defined only in the sets not in the logic...

if we can write "f->g" and "g->f", than the last 2 go in axioms set, and we can write "(f->g) and (g->f)" and "(f->g) or (g->f)" and "f<->g" that will be all "derivati dagli assiomi" and will use for build other string

Rosario

09:50

for example this x→(y→z) = x→((x→y)→z) = y→(x→z) is this for me (x→(y→z)) ↔ (x→((x→y)→z)) ↔ (y→(x→z)) where "(a↔b) ↔ (a→b) ˄ (b→a)"

l4m2

= mean can rewrite

-> is the operation

Can define a<->b as ((a->b)->(b->a)->⊥)->⊥ then prove a<->a

Rosario

i defined ↔ as "(a↔b) ↔ (a→b) ˄ (b→a)"

l4m2

Same from a∧b = (a→b→⊥)→⊥

but = and ↔ are not defined as same thing

Also some system discuss "Under condition a, (a→b)→b". Here such thing all expressed as →

Rosario

10:12

this is on your file line 50
Pf. a∨b #
= (a→b)→b

this below is the why i can write ((a→b)→b) ↔ (a∨b) from

(a→b)→b \n
(¬avb)->b \n
¬(¬avb)vb \n
(a˄¬b)Vb \n
(avb)^(¬bVb) \n
(avb)

using the axiom for me (a ^ b)V c ↔ (aVc)^(bVc) and the axiom (a→b)↔¬avb

even use axiom ¬(¬avb) ↔ a^¬b

a^(¬bVb) ↔ a

l4m2

I proved at last that every correct formula provable

Rosario

10:28

in pratice ↔ is as you = only there is (a=b) = a->b and b->a

above a=b dont mens a is true or b is true

« first day (5077 days earlier) ← previous day next day → last day (61 days later) »

all rooms