Tessera

Folgen

잇창명 EatChangmyeong💕🐱

@pub.eatch.dev

*Encounter the Wider World* 🌉 bridged from ⁂ https://hackers.pub/@eatch, follow @ap.brid.gy to interact

191 Posts8 Follower 1 Folgt

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 6d ago

아 허탈해 어제부터 계속 뭐가 안되는거지 싶었는데 완전 엉뚱한 곳을 보고 있었어.....

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last wk.

TIL: `foo-flatten-good`은 되는데 `foo-flatten-bad`는 termination checker가 싫어한다

data Foo : Set where
foo : List Foo → Foo

foo-flatten-good : Foo → List Foo
foo-flatten-good (foo []) = []
foo-flatten-good (foo (x ∷ xs)) with foo-flatten-good x | foo-flatten-good (foo xs)
... | x' | xs' = x' ++ xs'

foo-flatten-bad : Foo → List Foo
foo-flatten-bad (foo []) = []
foo-flatten-bad (foo (x ∷ xs)) with foo-flatten-bad x
... | x' with foo-flatten-bad (foo xs)
... | xs' = x' ++ xs'

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last wk.

바보아그다ㅠㅠㅠㅠㅠㅠㅠㅠㅠ

Agda의 오류 메시지:

[검열됨]/regex.agda:148,1-12: error: [ShouldBeEmpty]
¬ ch ≡ ch should be empty, but that's not obvious to me
when checking the clause left hand side
Regex.with-328 N = N ch (no ())

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last wk.

나는 이 이야기를 무척 좋아한다 https://velog.io/@ainochi95/CSS의-새-로고-Color-rebeccapurple에-관한-이야기

CSS의 새 로고 Color: “rebeccapurple”에 관한 이야기.

어느 날, Geek News를 보다가 CSS의 새로운 로고여서 문득 관심이 생겨서 읽어보게 되었습니다.

velog.io

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2w ago

적어도 웹개발 생태계만 보면 ESM이 별다줄의 끝판왕이라고 생각한다 * ESM = **ES M** odules * ES = **E** CMA**S** cript * ECMA = **E** uropean **C** omputer **M** anufacturers **A** ssociation (지금은 아니지만)

잇창명@고정 게시물 EatChangmyeong💕🦋@eatch.dev · 2w ago

쿠폰을 '다운받는다'는 표현을 보면 항상 신기하다... 무릇 '다운로드'란 서버의 데이터를 내 기기에 파일의 형태로 저장하는 것인데 쿠폰은 그게 아니잖아!!

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 3w ago

내가 좋아하는 프로그래밍 언어 붐은 온다...

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 3w ago

님들의 최애 정렬 알고리즘은 무엇인가요??

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 3w ago

wilson's algorithm my beloved https://youtu.be/Y6Ijgl0iZb0

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 4w ago

> 마인크래프트로 회로를 만드는 잇창명 > 관측기가 펄스를 2번씩 쏴서 pulse divider를 찾아봄 > hopper-loop pulse divider > 그대로 만들었는데 왜 안되지 > 1시간을 날림 > 아 모르겠다 플립플롭이나 달아야지 > 위키: "구리 전구 쓰세요 ㅎㅎ" > ...

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 4w ago

오 여기서는 글 쓰고 수정이 되는구나 수정 기록도 볼 수 있나요?

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 4w ago

"여기를 누르세요" ← 이게 접근성에 나쁘니까 쓰지 말라는 말은 많이 들었는데 그거 말고 다른 이유도 있구나 신기하네... https://www.smashingmagazine.com/2012/06/links-should-never-say-click-here/

Example Domain

example.com

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last mo.

어떻게 라이브러리 이름이 CuTe ><

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last mo.

아 `pnpm up`으로 다운그레이드가 되네?? ㅋㅎ

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · last mo.

☘️ *`^C^R`* Agda "error: [Interaction.CannotRefine] Cannot refine" ☘️ "아니 왜" Agda "Cannot refine" ☘️ "이유라도 알려줘" Agda "Cannot refine" ☘️ "..." Agda "..."

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

저는 지금까지 Agda를 이유 없이 한글로 아그다라고 썼는데요, **아그들아**

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

큰일났다 아그다 안쓴지 너무 오래돼서 어떻게 쓰는지 다까먹었네... 이거 어떻게 증명하더라 코드 private variable a : Level A : Set a split : List A → List (List A × List A) split [] = ([] , []) ∷ [] split (x ∷ xs) = ([] , x ∷ xs) ∷ map (λ (fst […] [Original post on hackers.pub]

private
variable
a : Level
A : Set a

split : List A → List (List A × List A)
split [] = ([] , []) ∷ []
split (x ∷ xs) =
([] , x ∷ xs) ∷
map
(λ (fst , snd) → x ∷ fst , snd)
(split xs)

splits : ℕ → List A → List (List (List A))
splits zero [] = [] ∷ []
splits zero (x ∷ xs) = []
splits (suc n) xs =
concatMap
(λ (fst , snd) → map (fst ∷_) (splits n snd))
(split xs)

splits-length :
(n : ℕ) →
(xs : List A) →
All (λ ss → length ss ≡ n) (splits n xs)
splits-length zero [] = refl ∷ []
splits-length zero (x ∷ xs) = []
splits-length (suc n) [] with splits n [] | splits-length n []
... | ss | pxs = ?
splits-length (suc n) (x ∷ xs) = ?

*All Goals*

?0 : All (λ ss₁ → Data.List.foldr (λ _ → suc) 0 ss₁ ≡ suc n) (map (_∷_ []) (splits n []) ++ [])
?1 : All (λ ss → length ss ≡ suc n) (splits (suc n) (x ∷ xs))
_A.a_273 : Level
_A_274 : Set _A.a_273
_A.a_275 : Level
_A_276 : Set _A.a_275

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

내가 아그다 버그를 밟았다고 [1] [2]

Agda 컴파일러의 경고 메시지:

Stale holes detected

Agda returned no interaction points, but holes are still present in the file. This is a known Agda bug (agda/agda#2475, agda/agda#6871) that can occur with cached .agdai files built under --allow-unsolved-metas. To recover: delete the _build directory and reload, or make a small edit inside a hole and reload.

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

여러분 혹시 파이어폭스 안드로이드에서 URL 자동완성 기록 **하나** 만 지울 수 있나요??? 네이버를 들어가려고 nav를 치고 엔터를 누르면 자동완성이 `naver.me`로 돼서 너무 성가십니다.

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

useless as always

Claude Haiku 4.5의 대화 기록. "한국어 일반명사, 3글자, 마지막 글자가 '구'" 프롬프트에 대해 7초 동안 생각한 뒤 "안구, 탁구, 족구, 용구, 복구, 함구"라고 응답했다.

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

그러고보니까 F12를 누르면 `debugger;` 앞뒤에 시간 측정 로직을 넣어서 건드리면 스크립트가 강제 종료가 되는 사이트가 있었다

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

자기PR(pull request myself)

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

오랜만에 아그다를 설치했다!!!!

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

아니 윈도우 11 시계 앱은 업데이트 설치가 강제야? 도대체 누가 이런 의사결정을 한 건데?

윈도우 11의 시계 앱. 원래 시계 UI 대신 '시계을(를) 업데이트해야 합니다. 업데이트를 준비하고 있습니다...'라는 문구가 있다.

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

유튜브 STT 알고리즘이 바뀌었나? 한국어 자막이 못알아먹을 수준인데 (방송 특성상 말소리가 좀 많이 섞이긴 하는데 그래도 지금까지 저 정도로 못알아먹을 텍스트가 나오지는 않았음)

KBS '안녕하세요'의 한 장면. 유튜브에서 자동 생성된 한국어 자막이 다음과 같이 표시되고 있다:

더 갈길 가고 나는 집에 각하 2차 감사 이렇게 생각을 하고 잊어 버리는데 가끔은

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

(재밌는 사실) 저는 그룹명이 UNICODE라는 이유만으로 개인 플리에 넣은 곡이 있습니다.

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

아 OSSCA 신청안했는데 안붙었네 *트훔*

레몬그린 @bananamilk452.hackers.pub.ap.brid.gy · 2mo ago

연합우주 블로그 만들면서 제일 힘들었던거: 표준?을 찾기가 너무 힘들었어요.... 당장 마스토돈/미스키에서 홈/팔로워/공개 이런 범위들 설정하는 것조차도 어디 적혀있는 곳이 없어서 제가 fedify 문서 어딘가에서 찾아서 겨우 구현했어요 (사실 제대로 구현한 건지도 모르겠음) 그거랑 멘션이나... 답글 어떻게 달아야하는지. 답글 주체를 어떻게 cc나 to에 넣어야하는지... 이런 것도 뭔가 알려진 문서?를 찾기가 힘들어서... 혹시 이런게 적힌 문서가 있나요?

레몬그린 @bananamilk452.hackers.pub.ap.brid.gy · 2mo ago

궁금한 점: Misskey의 커스텀 이모지 리액션 같은 건 일반적인 ActivityPub Lookup으로는 안 들어오나요? 꼭 Misskey API로 노트 조회를 한번 더 해야 가져올 수 있는 정보인가요?

잇창명 EatChangmyeong💕🐱@pub.eatch.dev · 2mo ago

컬쳐랜드를 오랜만에 쓸 일이 생겼는데 얘네들 보안정책이 너무 짜증난다... 비밀번호 자동 입력을 막아놔서 패스워드 매니저도 못쓰는데 6개월 동안 안 들어왔으면 비밀번호 변경이 **필수** 라고? 그와중에 `&#`이나 `\` 입력도 안돼?

$컬쳐랜드 모바일 웹 서비스의 장기 미로그인 회원 비밀번호 변경 화면. 비밀번호 규칙은 다음과 같다: * 8~20자의 영문, 숫자, 특수문자 조합 (` 또는 ' 및 공백 사용 불가) * 3자리 이상 연속·동일한 영문/숫자/특수문자 사용 불가 * 아이디, 휴대전화 번호, 생년월일 사용 불가 * &#(순서대로 나열), \, ￦은 사용 불가$