id: c4587af491a4417a84df8fe025080d2c
parent_id: 06fad9c02a134ddeaeb7fca090f23b79
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1697029705717
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"he FOL\\\n\\\n\"],[1,\"In the first-order language we assume a unary predicate P, a binary predicate T and a binary function symbol @. P(t) asserts the provability of t, T(t, τ) asserts that term t has type τ. @(t, s) represents function application `t s`. The optimisations in step 3 can optimize naive translations using these symbols, for instance turning `P(@(@(c, t), s)` into `c(t, s)`.\\\n\\\nA FOL axiom is a pair of a FOL formula and a constant (label). We translate CIC0 to a set of FOL axioms.\\\n\\\n\"],[0,\"#### Exp\"]],\"start1\":24224,\"start2\":24224,\"length1\":16,\"length2\":493},{\"diffs\":[[0,\"pe is...)\\\n- \"],[1,\"Mutually inductive types are exported separately for each constituent inductive type\\\n- The Coq construct `cofix` is exported to `fix` in CIC0 with a special flag that affects the evaluation algorithm\\\n- Modules and functors are not exported\\\n- Universe constraints on Type are not exported; proofs of paradoxes in the standard library are also filtered out and not exported\\\n- Records are already translated to inductive types by Coq, and therefore exported as such\\\n- Existential metavariables are not exported - it is not currently possible to use the hammer if uninstantiated existential metavariables are present in the proof state\\\n\\\n\"]],\"start1\":25288,\"start2\":25288,\"length1\":12,\"length2\":645}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-11T13:14:54.731Z
created_time: 2023-10-11T13:14:54.731Z
type_: 13