Have you looked into Idris2 at all. While looking into these theorum provers, it... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		aeonik on Oct 27, 2023 \| parent \| context \| favorite \| on: Lean4 helped Terence Tao discover a small bug in h... Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming. Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving. https://github.com/idris-lang/Idris2

atomicnature on Oct 27, 2023 [–]

That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.

iso8859-1 on Oct 27, 2023 | [–]

There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...

Consider applying for YC's Summer 2026 batch! Applications are open till May 4
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact