-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _".
The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach.
[1] https://github.com/pigworker/Samizdat/blob/main/ExampleSeman...
> I could not write this stuff. It looks simple but it isn't.
True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.