id: 74304a14931d4a0e81c7a0b54f6d0f93
parent_id: d35dd6162d2e4e2a96b3416410e84368
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1697031983133
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"L terms.\"],[1,\"\\\n\\\nCoqHammer uses type guards in its translation.\\\n\\\nThe definitions of `F, G, C` are given in the paper. They do pretty much what you expect, given that this is a type guards encoding that assumes proof irrelevance.\"]],\"start1\":26320,\"start2\":26320,\"length1\":8,\"length2\":221}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-11T13:54:54.699Z
created_time: 2023-10-11T13:54:54.699Z
type_: 13