Pinned toot

Martin Loaf

General recursive
Specific recursive

A proof assistant but with clippy

🤝
camels

"Combines the constructivism of intuitionist logic with the duality of classical logic" sounds interesting. Wish I could read

I found sequent calculus rules online, but I do not understand them. They don't seem like the usual format that typing rules have. I can't really wrap my head around what they're supposed to mean

Does anyone know of like an "informal" explanation of linear logic?

me if I were a commutative diagram: (commutes)

I wonder if HoTT "scales" to like, analysis and whatnot

If you pick up any math book and try to translate a proof into a proof assistant, it's not just tedious, it's hard. Unless you happen to pick up HoTT, I guess, and you happen to be using a proof assistant based on constructive type theory

Squiggle equality ~

Get it. Do you get it. It's cause small step semantics, big step semantics. Do you get it

One small step for theory, one big step for implementation

Someone do this

If Coq had Isar, and rewrite rules, that would be like, awesome

Or, sneaky anti-LEM

Sneaky LEM

I would not refute LEM. I would instead prefer to have a rule which all agreed was intuitive and obviously true, which nonetheless refuted LEM

I am like copy, paste, s/blast/iprover, "I am like a mathematician now, probably"

I also hooked up Isabelle's case splitter and induction tactics, but it's anyone's guess whether these actually work cause they rely on classical theorems, and I just lied instead and fed it contrapositivity

For unknown reasons, I have hooked up Isabelle/IFOL to Isabelle's simplifier and plonked on a constructivized version of HOL's set theory (I replaced "by blast" with "by iprover" and removed some classical lemmas which were unprovable)

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.