Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
Reply to @tak4
たかし@tak4 (2026-01-10 16:48:39)
ホームタイムラインは見えないけど自分のプロフィールから投稿を辿り返信
vvykg@vvykg@misskey.flowers (2026-01-10 16:48:03)
画像を投稿
---Attachments---
https://s3.misskeyflowersusercontent.jp/media/885c71a7-626c-4b10-9060-5b43c953a20c.webp
たかし@tak4 (2026-01-10 16:46:50)
tuskyから投稿
たかし@tak4 (2026-01-10 15:47:13)
guiソフトは想定外のことが起こるとヒステリーみたいにアプリ全体が落ちるものが多い。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-10 11:50:27)
ListとVecは多分特別に難しいから別のにしよう。。。
SASANO Takayoshi@uaa@social.mikutter.hachune.net (2026-01-10 09:53:49)
電報が廃止されていく（もう廃止された？）にあたり、電報特有の言い回しというのも廃れていくのだろうね。もう廃れているという気もするけど…文字数ごとの料金とかカナ数字しか使えないといった制約はなくなっているはずだから。
コシヌケ1040@ksnk@pawoo.net (2026-01-10 09:50:33)
そろそろねるか。
Reply to @uaa@social.mikutter.hachune.net
SASANO Takayoshi@uaa@social.mikutter.hachune.net (2026-01-10 09:48:51)
手元の練習帳（令和３年１１月１日版）では種類：イワイ 特別取扱：（なし） 局内心得：デラツクスオシバナになってる。
SASANO Takayoshi@uaa@social.mikutter.hachune.net (2026-01-10 09:47:25)
メモ：今の和文電報練習帳と少し前のでは違うみたいだな…
（しかもgooブログなので検索しても簡単に見つからない…）
https://web.archive.org/web/20251106090950/https://blog.goo.ne.jp/bushidajp/e/7f653abe1ad0ca87d66a24e989c8c727
Rikuoh Tsujitani@riq0h@letter.mystech.ink (2026-01-10 09:10:04)
美服を着て心も錦なら攻守最強になれる🤩
コシヌケ1040@ksnk@pawoo.net (2026-01-10 05:48:49)
現XにしてもYouTubeにしてもメルカリにしても、そこで流通する物の質を問はずに利用者から手数料を取る、ってのが儲けの最適解になってるんだらうね。鉄火場は胴元が一番儲かるやうに出来てゐるものだ。
Laura Manach :bongoCat:@cmconseils@mastodon.social (2026-01-10 05:33:01)
You can say "Have a nice day" without any problem, but using the phrase "enjoy the next 24 hours" can sound slightly threatening.
コシヌケ1040@ksnk@pawoo.net (2026-01-10 04:54:12)
都心いくと食べ物が高いから、いつも逃げるやうに日高屋に行く。いい店だよねぇ。
Reply to @aaa
🦉@aaa (2026-01-10 04:42:39)
寝て起きてから考えよう
🦉@aaa (2026-01-10 04:37:51)
android端末を持っていないからテストできていなかったけどtuskyはavatarが無いと落ちるらしい
でもtokodonとtubaはavatarが無いときユーザー名の頭文字を表示してくれるからabout:blankにするのももったいない気がしてしまう
佐々木@nounashi7298@social.nekokawa.net (2026-01-10 00:57:36)
音楽の歌詞を読まずにメロディしか聴いてない問題、どう受け止めるべきなのか
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-10 00:34:20)
このあと、Listとその長さの依存和とVecが同型であることを示して、同型をパスにして変換できるようにするのをやってみたい
たぶん、Listで定義した非効率で Vec からは定義しにくい rev を Vec から間接的に使えるようになるはず…
たかし@tak4 (2026-01-10 00:17:29)
人を見る時、人の言動はストレスの影響を受けてゐることを前提にしたい。
完全にストレスの無い理想的な状態での言動を想像してみる。特にsnsはストレスのはけ口になりやすいので、そのままの印象で捉へると本人の心の形が分からなくなる。
Reply to @tak4@mstdn.y-zu.org
@risahana@mstdn.jp (2026-01-10 00:04:18)
@tak4 ありー🦋 🦋 🦋
Reply to @risahana@mstdn.jp
たかし@tak4@mstdn.y-zu.org (2026-01-10 00:03:46)
@risahana ハローでっす
@risahana@mstdn.jp (2026-01-10 00:00:12)
ハロー！夜の民＼(^o^)／
たかし@tak4 (2026-01-09 23:58:36)
oepnbsdのデスクトップの背景を真っ黒にしてuiは白ベースだったのも良くなかった。
黒い背景に白いものがあると眼に突き刺さる感じ。
デスクトップの背景を # 808080 にしたら良くなった。xtermの背景も白より少しだけ薄い色にした。
uiを暗くしないのは暗色だと低輝度で見づらいことがあるのと、拘りで色々なものを暗色に統一したくなるから。
コシヌケ1040@ksnk@pawoo.net (2026-01-09 23:35:12)
各国民の自由度はインターネットの自由度で測れるのではないか。と最近考へてみたりする。
Coro@Coro@mstdn.maud.io boosted:
@mattferrell@mastodon.social (2026-01-09 22:17:05)
#FunFactFriday: Attempting to lower diesel use, the Maldives are using floating ocean solar-battery microgrids. Will this become the model for other islands? Source: https://www.pv-magazine.com/2026/01/08/maldives-microgrid-project-with-floating-solar-becomes-model-for-island-renewables-projects/
---Attachments---
https://files.mastodon.social/media_attachments/files/115/865/329/634/713/403/original/70e272ad3cd2c779.jpeg
Matt Ferrell@mattferrell@mastodon.social (2026-01-09 22:17:05)
#FunFactFriday: Attempting to lower diesel use, the Maldives are using floating ocean solar-battery microgrids. Will this become the model for other islands? Source: https://www.pv-magazine.com/2026/01/08/maldives-microgrid-project-with-floating-solar-becomes-model-for-island-renewables-projects/
---Attachments---
https://files.mastodon.social/media_attachments/files/115/865/329/634/713/403/original/70e272ad3cd2c779.jpeg
コシヌケ1040@ksnk@pawoo.net (2026-01-09 22:09:18)
政府にインターネットを遮断されたイラン国民に、イーロンマスクがスターリンクを貸してゐるらしい。人口衛星を持ってゐる富豪はさすが強い。
ところで、万が一アメリカ政府がネットを遮断したとき、スターリンクはどういふ扱ひになるのだらう。スペースXはアメリカの民間企業だよねぇ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:58:35)
「等しいこと」については「真」か「偽」しかなくて中身がなかった。中身がないから構成する手段もなかった。だから等しさの証明は構成的ではなくて操作的にならざるをえなかった。この問題を解決した Cubical Agda は最強に違いないので色々やってみたいところ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:44:05)
Agdaだと命題を表現するのに data で型定義をするということがよく行われ、命題の証明は型に対応する証明オブジェクトを構成することによって証明が行うのが自然なアプローチという感じになってる。
しかし、同一性の証明に関しては扱いにギャップがあり sym, cong, subst, rewrite 構文などを使ってうまく命題を操作するプログラムを書く感じになってしまう。
これが Cubical Agda だと、同一性の証明は対応する証明オブジェクト(Path)を構成することになるので、他のアプローチと同じ方法で取り組むことができるのですごい。
コシヌケ1040@ksnk@pawoo.net (2026-01-09 21:42:34)
'00年代にWindows向けの豊かな無償ソフトウェアを幾つも使ってきた所為か、ちょっと画像を縮小するだけのスマホアプリまでことごとく広告有りなのは、なんだかなぁと思ってゐる。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:35:45)
「同一性」が第一級のオブジェクトじゃなかったという問題が、HoTTによって解決され Cubical Agda では「同一性」を式の操作ではなく「同一性」を表すデータを構成する形で証明できるようになったというところが嬉しさの核であるように思う。
Older Notes