id: d1b3b8275b864381ba4ac9f2874ebd4f
parent_id: 40fb34b144f04606a9672be8176ac27b
item_type: 1
item_id: 6e98d35480c9412c8a1390f17cda32ea
item_updated_time: 1681837668917
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"oq (\"],[-1,\")\\\n- [ ] Hurd (2003)?\"],[1,\"Czajka, L., Kaliszyk, C., HaTT 2016)\\\n\\t- Base for the Hammer for Coq translation\\\n- [ ] First-order proof tactics in higher-order logic theorem provers (Hurd, 2003)\\\n- [ ] History of interactive theorem proving (Harrison, J., Urban, J., Wiedijk, F., 2014)\\\n- [ ] Program extraction within the Coq proof assistant (Letouzey, P., 2004)\"],[0,\"\\\n\\\nNo\"]],\"start1\":733,\"start2\":733,\"length1\":28,\"length2\":337},{\"diffs\":[[0,\" (Curry)\"],[1,\"\\\n[Lean type system overview](https://leanprover.github.io/papers/lean4.pdf)\"],[0,\"\\\n\\\nTimeli\"]],\"start1\":1187,\"start2\":1187,\"length1\":16,\"length2\":91},{\"diffs\":[[0,\"s 1-15\\\n1\"],[-1,\"6\"],[1,\"8\"],[0,\"/04: Ham\"]],\"start1\":1313,\"start2\":1313,\"length1\":17,\"length2\":17},{\"diffs\":[[0,\" Coq\"],[-1,\", pagina's 16-31\\\n17/04:\"],[1,\" (finish);\"],[0,\" Jas\"]],\"start1\":1337,\"start2\":1337,\"length1\":31,\"length2\":18},{\"diffs\":[[0,\" lezen\\\n1\"],[-1,\"8\"],[1,\"9\"],[0,\"/04: A S\"]],\"start1\":1403,\"start2\":1403,\"length1\":17,\"length2\":17},{\"diffs\":[[0,\"'s 1-15\\\n\"],[-1,\"19\"],[1,\"20\"],[0,\"/04: A S\"]],\"start1\":1447,\"start2\":1447,\"length1\":18,\"length2\":18}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-04-18T17:13:06.615Z
created_time: 2023-04-18T17:13:06.615Z
type_: 13