New answers tagged

2

There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names $V$ and define the context $\Gamma : V \rightharpoonup S$ as a partial function from the set of variable names to the set of types. $\mathrm{dom}(\Gamma)$ is then the subset of $V$ on which $\Gamma$ is defined, i.e. the variables ...


3

The initial assumption about such types having at most countably many elements is false. We can use inductive types to define a non-countable type, namely the countably branching trees: (* Countably branching trees. *) Inductive Tree : Type := | Leaf : Tree | Node : (nat -> Tree) -> Tree. Lemma nocycle (t : Tree) : forall (f : nat -> Tree), t = ...


Top 50 recent answers are included