id: bbdb15d0a980414c8153ff73db4c0e4e
parent_id: cb2fd1a53818458aac5b359c4640127b
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696867081178
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\" A type cast\"],[1,\"\\\n\\\nForms of declarations:\\\n\\t- A definition `c = t : tau`; definition of a constant `c` saying `c` is equal to `t` and has type `tau`\\\n\\t- A typing declaration `c : tau`; declaration of a constant stating it has type `tau`\\\n\\t- An inductive declaration `I_k(c:tau := c1 : tau1, c2: tau2, ..., cn: taun)`\\\n\\t\\t- Example: `I_1(List: Type -> Type, nil: (ΠA: Type, List A), cons: (ΠA: Type, A -> List A -> List A))`.\\\n\\t\\t\\\nAn _environment_ is a set of declarations. We assume an implicit global environment `E`, which is assumed to contain appropriate typing declarations for the logical primitives.\\\nA _context_ is a list of declarations of the form `x: t` with `t` a term of CIC0 and `x` the declared CIC0 variable.\"]],\"start1\":20973,\"start2\":20973,\"length1\":12,\"length2\":711}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-09T15:58:35.098Z
created_time: 2023-10-09T15:58:35.098Z
type_: 13