so I gave this to chatgpt and asked to infer meaning
it explored some guess that went too far, told to try another guess and to re-read the first line
and so it infered sequential branch merging equations
... I guess I found my new PLT denotational assistant
The example I liked the most that it's possible to define Option, List and NonEmptyList with a single type! This way one can write functions like map, head only once for all three types. And you can pass a list with length 1 to a function that expects an option since they are essentially the same type.
I hope we see this being implemented in different languages in the future.
If you want to read more on this, here is the link:
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.17
**Theorem proving with the real numbers**
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-408.html
by John Robert Harrison
November 1996
The author used #HOL to formalise real numbers, including metric, sequences and limits, continuity and differentiation, power series and transcendental functions, integration.
There is also a #CAS and IEEE floating standard verification tools.
Nature Programming Language
Lobsters
jnpn
YAYAFA
TKHUNT
Aiono
terrorist :: Feline
Lobsters