|
|
|
|
|
||
|
||
すべて | グループ指定なし | C#&.NET海外 | C#&.NET日本
2025-05-03
10年前のハーフマラソンの呪縛を解いた & 2025年4月のランニングの記録
2025 / 5
2025-05-05
QRコードの誤り訂正がどれだけ優秀かを実感できるウェブサイト「QR is cool」、QRコードはかなり改変されても元の情報を維持できる
gigazine.net
Rコードには誤り訂正機能が組み込まれており、一部が汚れていたり破損したりしていても元の情報を読み取れるようになっています。そんなQRコードの誤り訂正能力を実感できるウェブサイトが「QR is cool」で、自分でQRコードの一部を改変しながらどれだけ元の情報を保てるのか試すことができます。
App | QR is cool
https://qris.cool/
QRコードの誤り訂正能力は「レベルL」「レベルM」「レベルQ」「レベルH」の4段階に分かれており、レベルLなら最大約7％、レベルMなら最大約15％、レベルQなら最大約25％、レベルHなら最大約30％が欠損しても元の情報を保つことができます。
sdpaninf 2025-05-05 00:00 読者になる
広告を非表示にする
もっと読む
コメントを書く
QRコードの誤り訂正がどれだけ優秀かを実感できるウェブサイト「QR is cool」、QRコードはかなり改変されても元の情報を維持できる
2025-05-03
_ 絶望の日
ビックカメラの上に移転中のル・シネマでオリヴィエラの未見だった『絶望の日』。
なんか有名な文学者が自殺する映画としか知らないで行ったが、最近では珍しく多分ほとんど眠ってしまった。が、不快な入眠（未来世紀ブラジルとか、退屈で睡眠へ逃避）というのとは違って、実に心地よかった。これだけ心地よいのだから間違いなく名画だが記憶がほとんどない。
理由は明々白々で、パルジファル前奏曲がほぼ全編に使われているのだが、テンポが極端に遅い。記憶にある録音でこんなに遅いのは聞いた覚えがないからポルトガルの楽人によるものか。
その遅さに混乱しているところにもって移動中の馬車の車輪の回転を延々と映す。くるくる回転する車輪を眺めているうちに催眠術にかけられたのだ。間違いない。
途中、これも何度かトリスタンとイゾルデの前奏曲の冒頭のトリスタン和音が入る。これは実に良い塩梅なのでトリスタン和音を楽しみにしていると、また極端に遅いパルジファルとなり催眠術にかかる。
そうやって、金を求めて何度も爵位を要求しては断られて、最終的には子爵となるが、年金についてまた何度もやり取りが発生する。
息子の病気を診てもらうために遠方の医師に使いを出しては断られるというのを繰り返す。ついに医師が来訪することとなる。そこでまた催眠術が流れて、結局どう診断されたのかどういう治療方針となったのかが謎のまま時が過ぎる。
そして銃声。
最後、無調の室内楽が流れる。これは名曲だが、誰の作品なのだろうか。
おもしろかった。
追記）最近は近年のバイロイトのビシコフやヘラスキャサードの11分後半～12分前半のやつを聴きなれているからで、さっきショルティのを聴いたら死ぬほど遅くて12分50秒台。数十年前はこれを聴いていたと考えると、当時は全然普通だったのかも。というわけでおそらくショルティを使っている可能性が
en-us
雑記／備忘 上下左右
May 2025
Meta AI App
en-us
2025-04-27
IaCオーケストレーションを支援するSymphony
Azure Pipelines GitHub Azure
Share on Tumblr
はじめに
IaCはBicepなりTerraformなりなんでもいいですが、ソースコードを管理するレポジトリをアプリケーションと一緒にするか、インフラのみのレポジトリにするのか悩ましいと思っています。格納したとしても、デプロイするときのパイプラインを作るのもなかなかめんどくさいと思っていました。
そんなある日、GitHubのレポジトリあさっていたら、MicrosoftからSymphonyというツールがあることを知りました。宣伝を見かけたことはないですが、そこそこコミットもされているようです。
github.com
これで万事解決というものではないですが、デプロイ用のスクリプト作るのめんどくさいなーとか思っている人は使ってもいいと思います。
GitHub/Azure DevOpsサポート
チームプロジェクトもしくはレポジトリは存在しない状態で作らなくてはならない
Terraformの場合Azure Storageアカウント必要（Bicepでもなぜかつくられるけど）
GitHubの場合はPull Request検証してくれるが、Azure Pipelinesはやってくれない（自分で登録して工夫しないといけない）
サポートはLinux(Ubuntu)のランナーのみ
クライアントはWSL内での実行を推奨（bash/zsh）
git remoteはちゃんと書き換えよう
Service Principal作成権限が必要です
初期構築
実行してみます。azure cliでログインして、symphonyのレポジトリをクローンした後、git remoteを消してください（git remote remove orgin）。そのままで
Google Developer Groups on Campus（旧 GDSC）東京都立大学 2 期リードの Aoi Ohta さんをご紹介
2025年4月25日金曜日
前回の記事では、GDGoC Waseda 創立者の Rose Niousha さんをご紹介しました。今日は、GDGoC TMU 2 期卒業生の Aoi Ohta さんにインタビューを行いました。
自己紹介をお願いします！
こんにちは、Aoi Ohta（ハンドル名：marsh_mallow）です。2022 年 10 月 〜 2023 年 9 月までの 1 年間、GDSC TMU (Tokyo Metropolitan University・東京都立大学) の リード（代表）を務め、リード卒業時に「チャプター再構築部門があったら1位」という大変光栄な評価をいただくことができました。任期中の具体的な経験については、同期や後輩リードからの「具体的にどう再構築したのか知りたい」という声にお応えして、この記事にまとめています。
もともとは高専出身ですが、電気情報工学科で電気電子分野を中心に学んでいましたので、ソフトウェア開発にはほぼ全く触れることのない高専時代を過ごしていました。2021 年春に高専を卒業後は、やりたい研究があったので都立大の情報科学科に編入したのですが、やりたい研究がソフトウェア開発関係ではなかったので、相変わらずソフトウェア開発とはほとんど無縁でした。ですが、高専・大学でロボコン（NHK高専ロボコン/学生ロボコン）のチームに所属し、マイコンを用いたロボットの制御や電子回路系の担当として計 5 年ほど活動していました。ですので、ソフトウェア開発の経験は無いものの、コードを書くことや他の人と一緒になにかモノをつくることに関する経験はそれなりにある、というような状態でリードに就任しました。
「IT 系モ
Skip to main content Skip to Ask Learn chat experience
Ask Learn Ask Learn Read in English Save
Note
Access to this page requires authorization. You can try signing in or changing directories.
Access to this page requires authorization. You can try changing directories.
2024-09-25
Feedback
en-us
2025-04-11
_ 言語モデルの物理学
https://joisino.hatenablog.com/entry/physics
むちゃくちゃ面白かった。ちゃんと原文も読みたさがある
(12:12)
[ツッコミを入れる]
Skip to main content Skip to Ask Learn chat experience
Ask Learn Ask Learn Read in English Save
Note
Access to this page requires authorization. You can try signing in or changing directories.
Access to this page requires authorization. You can try changing directories.
2024-09-25
Feedback
en-us
■ 追記：一部訂正（4月5日）
「連載論文(6)〜(9)の4本」を読み込ませていたつもりだったが、よく見たら、誤って(7)は違うファイル（校正時に作成した追記分の短いファイル）を入れていたことが判明。
Claudeのプロジェクトナレッジの設定
結果として1970年代前後の米国発の話などが含まれていなかった。「data subject」の誤訳の話だけ持ち出してくるのは変だなとは思った。
というわけで、Claudeのコンテキスト容量の都合から、必要な範囲が収まらない。いずれClaudeが進歩してこの制限は解消されるであろうが、現在のところ、論文の圧縮版を作るしかなさそうだ。
2025-03-14
Encrypted Client Hello の実装
TLS
ECHをHaskell tlsライブラリに実装した話。先に「Encrypted Client Hello の仕様」を参照のこと。Haskellで実装した経験談なので、Haskellの知識を前提に書く。
ライブラリの構成
バックエンド・サーバの設定情報である ECHConfigList は、DNSを通じて提供され、TLSクライアントとTLSサーバで利用される。ECHConfigList の型や、その符号器/復号器をどのライブラリで実装するか決める必要がある。
tls ライブラリをECHに対応させると、ECHConfigList を利用するのは当然である。僕の希望としては、IIJが開発している DNS検索コマンドdug で HTTPS RR を検索したときに、ech パラメータが16進数表記されるのではなく、ECHConfigList を利用してユーザに分かりやすく表示されるようにしたい。
dug は、HTTPS RR を提供する dnsext-svcb ライブラリに依存している。ECHConfigList を tls から提供すると dnsext-svcb が tls に依存するし、逆もまたしかりである。両者は本来独立であるので、この依存関係が発生するのは嬉しくない。そこで、依存するライブラリの数が少ない ech-config というライブラリを新たに作り、そこに格納することにした。
ECHConfigList には HPKE のパラメータに関する情報が含まれている。ech-config が、新たに作成する hpke ライブラリに依存すると、単なる型情報を提供する ech-config が、暗号ライブラリ crypton に依存してしまう。これは避けたい。
という訳で、ECHConfigLis
この広告は、90日以上更新していないブログに表示しています。
Gemini Advanced の新機能 Deep Research が日本語でも公開
この広告は、90日以上更新していないブログに表示しています。
この広告は、90日以上更新していないブログに表示しています。
HDD データセンタ用の HDD の中古 42234 合計 28 TB。ebay でデータセンタで使われてた中古 HDD 14TB を二個買った。これまでもデータセンター用の HDD を ebay で買ってきたけどとてもコスパ良い
それでも10進小数をデフォルトにすることは意味がある
Bug Catharsis
2024年03月27日
noteの方に移行します
livedoor blogはずっと使わせていただいて愛着もあるのですが、https対応の予定が今後もない、という状態が続くようでもあるので、noteの方に引っ越します！
（そしてクレディセゾンでの5年間の活動の振り返りを投稿しました）
クレディセゾンでDXを進めてきた5年間を振り返る
お知らせ
by lalha
お知らせ (5)
noteの方に移行します
2024年03月
次世代3Dコンテントパイプライン開発室
読者になる
よくわかりません
読者になる
Radium Software
読者になる
naoyaのはてなダイアリー
読者になる
chokudaiのブログ
読者になる
lethevert is a programmer
読者になる
あけてくれ -- おれカネゴンの『算数できんのやっぱり気にしすぎとや』日記
読者になる
ものがたり(旧)
読者になる
Cheap Air Tickets
Dental Plans
Free Credit Report
fashion trends
Online classifieds
2024-02-01
Arm laptop
なんかいいやつないかな → ない
Cortex-X2 とか X3のが欲しいのだった。もちろん X4 でもいい。このぐらいになればもうx86に追い付いて普通に使えるのではという気がしたので。
Androidはある。
Wikipediaを見れば一覧あったわ。
https://en.wikipedia.org/wiki/List_of_products_using_ARM_processors
Cortex-X2
MediaTek Dimensity 9000
Qualcomm Snapdragon 7+ Gen 2, 8(+) Gen 1
Samsung Exynos 2200
Cortex-X3
MediaTek Dimensity 9200,
Qualcomm Snapdragon 8 Gen 2
Surface のは Qualcomm ので、残念ながらCortex-X1らしい。
手元のスマホはSnapdragon 888で Cortex-X1 だった。(Snapdragon 888 は Gen8 とは違うという学びがあった)
新しめの Arm Chromebookは
Kompanio 520 → ASUS Chromebook CM14 https://jp.store.asus.com/store/asusjp/ja_JP/pd/productID.5767035600/varProductID.5767035600/categoryID.4963963700
Kryo 468 → Acer Chromebook Spin 513 https://www.acer.com/jp-ja/chromebooks/acer-chromebook-enterprise-spin-513-cp513-1h-cp513-1hl-r841l
hyuki 2019-01-06 23:42 読者になる
tanakh 2020-08-31 03:29 読者になる
Generated by tDiary version 5.2.4
Powered by Ruby version 3.2.2-p53
今日は Rust.Tokyo 2023 の日です
2023 / 10
▼ ▶
2012
2012 / 10
▼ ▶
2011
2011 / 8
▼ ▶
2010
2010 / 2
2010 / 1
▼ ▶
2009
2009 / 11
2009 / 10
2009 / 9
2009 / 8
2009 / 7
2009 / 6
2009 / 5
2009 / 4
2009 / 3
2009 / 2
2009 / 1
▼ ▶
2008
2008 / 12
2008 / 11
2008 / 10
2008 / 9
2008 / 8
2008 / 7
2008 / 6
2008 / 5
2008 / 4
2008 / 3
2008 / 2
2008 / 1
▼ ▶
2007
2007 / 12
2007 / 11
2007 / 10
2007 / 9
2007 / 8
2007 / 7
2007 / 6
2007 / 5
2007 / 4
2007 / 3
2007 / 2
2007 / 1
▼ ▶
2006
2006 / 12
2006 / 11
2006 / 10
2006 / 9
2006 / 8
2006 / 7
2006 / 6
2006 / 5
2006 / 4
2006 / 3
2006 / 2
2006 / 1
▼ ▶
2005
2005 / 12
2005 / 11
2005 / 10
2005 / 9
2005 / 8
2005 / 7
2005 / 6
2005 / 5
自転車に再び乗り始めた
週末に気軽に自転車で出かけられるようになりました
10/1/2022, 1:38:23 PM
カリフォルニアで運転免許を取った
カリフォルニアのドライバーになりました
9/17/2022, 3:06:25 PM
カリフォルニアで車を買った
アメリカでミニに乗るやつになりました
9/10/2022, 6:39:13 PM
引っ越し先へ入居した
カリフォルニア州民になりました
9/5/2022, 6:25:09 PM
引っ越し当日になった
いよいよ引っ越しの日になりました
9/4/2022, 6:56:17 PM
引っ越し業者を探して荷物を梱包した
大陸横断引っ越しで荷物を運んでくれる会社を探しました。
8/31/2022, 11:07:33 PM
カリフォルニアの引っ越し先を決めた
カリフォルニアでどこに住むか決めました。
8/13/2022, 3:16:04 PM
カリフォルニアで引っ越し先を探した
カリフォルニアへ出かけてアパートの内見ツアーをしてきました。
8/7/2022, 2:34:11 PM
カリフォルニアへ引っ越そうかなと思った
カリフォルニアへ引っ越すことにして、場所を決めて内見ツアーを組んでみました。
7/31/2022, 12:13:41 PM
転職した
ソフトウェアエンジニアとして再出発します。
5/15/2022, 9:00:00 PM
壁に埋め込まれている電気のスイッチをHomekit対応のものに入れ替えた
スマートホーム的な何かをもう少しやってみるために、壁のスイッチを取り替えてみた。
1/17/2022, 12:24:09 PM
米国永住権（グリーンカード）取得顛末記 <2018-2021>
ごく普通の日本人ソフトウェアエンジニアが就労ビザで米国に渡って8年、とうとう永住権を取得するまでの長くて読み応えのない感想文です。
その後, 国立天文台暦計算室のページを見付けた.
2022-08-08
データ解釈学入門を読んだ - 2022 夏休み
統計検定2級や Kaggle で学んだものたちの隙間を埋めてくれる良い本だった。どことは言わないが、読んでいる途中に仕事のことを思い出す記述があり背筋がピンと伸びた。以下雑多なメモ。
分析者のためのデータ解釈学入門 データの本質をとらえる技術
作者:江崎貴裕
ソシム
Amazon
測りやすいデータが選ばれがち。
データを歪めるモチベーション（犯罪件数、いじめ件数は少なくレポートしたい）
(大きな声で何度でも）データの前処理は一番時間がかかる。手を抜かない。1つ1つの処理前後で正しいか必ず確認する。決してまとめて処理しない。
多重検定に注意。過去にこれやってたな。
HARKing, p-hacking これは・・・
数々の認知バイアス
higepon 2022-08-08 14:44
April 2022
1 2
3 4 5 6 7 8 9
10 11 12 13 14 15 16
17 18 19 20 21 22 23
24 25 26 27 28 29 30
都城のおすすめ整骨院 on あー実験うまくいかないー
22:22 21/11/20
ボレロ村上(村上原野)さんと constexpr のこと
去る2020年2月、縄文陶芸家にしてC++プログラマという希有な二つの顔を持つ人物がこの世を去りました。 ボレロ村上 (村上原野) 氏です。
正直なところ、陶芸家としての彼の側面については私はほとんど何も知らないに等しいです。
残された作品を見て何かを語れるほど芸術に通じているわけでもありません。
いつか機会があれば見に行こうと思っていた村上さんの作品を目にする最初の機会も、
昨年訪れた追悼展になってしまいました。
ただ、それでも私は、彼自身の登壇発表の資料 であったり、
そして何よりも縄文・陶芸に造詣の深い方々の記された幾つかの文章
（たとえば "なぜ若き縄文アーティストはリアルをめざしたのか〜村上原野くんを偲んで"）
によって、彼が一体何を成し遂げたのか、成し遂げようとしていたのかに触れることができています。
この夏にはクラウドファンディングで 作品集 も出版され、誰でも手にとって縄文アーティストとしての村上原野を知ることができます。
翻って、プログラマとしての村上さんが残した足跡は、
果たして C++ マニアでなくとも辿れるようになっているでしょうか。
彼がどのように異色の存在だったか、C++ の知識を前提とせずに書き留めておくことはできないものでしょうか。
この一年こういった疑問が頭を離れなかったので、拙いながら、
一筆残しておこうと思い書き上げたのがこの記事になります。
多忙にかまけて随分と遅くなってしまいましたが、ご容赦ください。
「constexprの人」
上のような趣旨を私が Twitter でつぶやいた時、いただいた反応の一つが好きだったので引用します。
「constexprをやたらと酷使することで有名だった人」の説明しづらさすこ
— ジャカルタ読み専ブラザーズ (@_
5...
次のページ
>>|
2017年07月20日09:00
カテゴリ
VALU
〓〓〓〓〓〓0
dankogai
コメント( 1 )
2017年03月19日16:30
カテゴリ
evalpark
Open Source
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2017年03月17日10:30
カテゴリ
evalpark
Open Source
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2015年12月03日19:30
カテゴリ
Math
〓〓〓〓〓〓0
dankogai
コメント( 1 )
トラックバック( 0 )
2015年07月11日13:30
カテゴリ
YAPC::Asia
Open Source
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2015年07月09日10:45
カテゴリ
YAPC::Asia
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2014年12月23日21:15
カテゴリ
ブロマガ
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2014年12月09日05:15
カテゴリ
弾本
Announcement
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2014年11月30日22:00
カテゴリ
ブロマガ
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2014年10月31日01:00
カテゴリ
ブロマガ
〓〓〓〓〓〓0
dankogai
コメント( 0 )
トラックバック( 0 )
2014年09月30日00:15
カテゴリ
ブロマガ
Announcement
〓〓〓〓〓〓0
dankoga
読者になる
% g++ -DV2 -O2 -c test.cpp ; g++
« お問い合わせ対応システム移行にともなう… はてなプライバシーポリシーの改定について »
はてなの各サービスの告知日記です。
読者です 読者をやめる 読者になる 読者になる
最新記事
携帯電話の回線を変更される方へのご案内
はてなプライバシーポリシーの改定について
はてなプライバシーポリシーの改定について
はてなIDのOpenIDサポート終了のお知らせ
はてなプライバシーポリシーの改定について
カテゴリー
はてなの日記 (632)
はてなアイデア日記 (600)
はてなグループ日記 (467)
はてなフォトライフ日記 (275)
人力検索はてな 日記 (254)
はてなアンテナ日記 (247)
はてなRSS日記 (241)
はてなカウンター日記 (167)
はてな使い方メールマガジン『週刊はてな塾』 (82)
はてなリング日記 (78)
はてなグラフ日記 (56)
はてなマップ日記 (42)
はてなロゴ日記 (32)
求人情報 (32)
はてなスクリーンショット日記 (19)
はてなグリースモンキー日記 (6)
月別アーカイブ
リンク
はてなブログ
ブログをはじめる
はてなブログPro
はてなブログをはじめよう！
hatenasupportさんは、はてなブログを使っています。あなたもはてなブログをはじめてみませんか？
はてなブログをはじめる（無料）
はてなブログとは
はてなの告知
Powered by Hatena Blog | ブログを報告する
ストック一覧を見る 閉じる
ログイン 閉じる
閉じる
限定公開記事のため引用できません。
読者です 読者をやめる 読者になる 読者になる
はてなブログに引っ越し
2021.04.12
はてなブログに引っ越し
2021年4月から、2020年以降の記事を含めて「はてなブログ」に引っ越しました。今後もよろしくお願いします。
設計者の発言（はてな版）
«オブジェクト指向開発もローコード開発も楽しい
2021年01月08日
2021年01月08日
マイナビニュース サイト改変「TECH+」を2/１より開始
マイナビは、マイナビニュースの中で主にBtoBビジネス領域を扱っている「企業ITチャンネル」「テクノロジーチャンネル」「IT Search+」を分離し、新たなメディア「TECH+」として2/1よりにリューアルオープンする。
リニューアルに関する資料はこちら
なお、2/1のリニューアル時点では広告メニューや仕様に変更は無い
Web
マイナビニュース サイト改変「TECH+」を2/１より開始
2021年01月
Copyright (C) 1999-2021
最近の冷凍食品うますぎてこわい
kansou
2020-08-28 18:09:12
【8/31まで】63時間のビッグセール Amazonタイムセールを淡々とチェックする【随時更…
山と旅とカメラのブログ。
2020-08-29 09:47:29
【話題沸騰中】軽量でお洒落なコマンドプロンプト拡張ライブラリ「Starship」を導入…
Hajimari Tech Blog| 株式会社Hajimari
2020-08-28 17:02:20
20/8/28 仮面ライダー555の感想 二階の排外主義者たち
LWのサイゼリヤ
2020-08-28 18:58:23
リリア の部屋
Green★Pharmacy
2020-08-29 01:09:56
結構散らかってるね(笑)、 まぁ、オレも人のこと言えないが(^_^;) てか、シルバー(>_<) いい子に育ったのぉ。
EVILが神宮大会で仕掛けてくるサプライズ
NJPW FUN
2020-08-29 08:00:07
安倍総理が辞任を発表して僕が考えた事。
超メモ帳（Web式）＠復活
2020-08-28 23:30:02
ラジオ
jmiyazaの日記（日々平安録２）
2020-08-29 10:38:58
救急車に乗ってみた
散るろぐ
2020-08-26 18:19:53
コロナのおかげで、自宅待機している新卒の子らには「このまま働かずに給料をもらい続けたい！」と強く思う子がいる…
日記 0829
Imaginantia
2020-08-29 05:17:55
んー。今日はいろいろあったいい日でした。主に現世の活動でした。 端的に言うとアートアクアリウムに行った後、川崎…
【ize訳】アイドル、華やかな照明が消えた後
サンダーエイジ
2020-08-28 23:10:55
アイドル、華やかな照明が消えた後 人格教育
意外かもしれないが、初デスクトップ。今回はサイコムというところで注文した。自作という選択肢もあったが、自分の不器用さをよく承知しているので(最近では液漏れで止まった時計を修理しようと分解して、再起不能にした)、BTOに。スペックは、
それに比較対象がThinkPad T460s (Core i7 6600U) 2 core 4 threadだからねえ
追記
サイコムから返事来た。送料着払いでボード２枚を返却したら、ボードぶんの代金を返金するとのこと。やさしい。
AgdaによるTaPL - Typed Arithmetic Expressions [Agda]
「プログラミング言語の基礎概念」(五十嵐2011)をAgdaでやっていた途中だが、 ここで ”Types and Programming Language” (Pierce 2002) の第8章 ”Typed Arithmetic Expressions” をAgdaでやることにする。
open import Relation.Binary.PropositionalEquality
using (_≡_; refl)
open import Data.Product
using (_×_; proj〓; proj〓; ∃; ∃-syntax) renaming (_,_ to 〓_,_〓)
open import Data.Sum using (_〓_; inj〓; inj〓)
Syntax of Terms
この章では同第3章で定義した算術式の言語に型をつける。 これは変数という概念が登場しない言語で、次のように定義される。
infix 10 succ_
infix 10 pred_
infix 9 iszero_
infix 8 if_then_else_
data Term : Set where
true : Term
false : Term
if_then_else_ : Term → Term → Term → Term
zero : Term
succ_ : Term → Term
pred_ : Term → Term
iszero_ : Term → Term
五十嵐(2011)はこれに近いML1という言語を定義しているが、その言語への型付けを扱っていない。 しかし変数がないため型環境について考えなくてよいという単純さがあって、 最初に型付けの証明をする