blob: 3bc44f6462353c7b95560696898e92a7f3436a27 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
+++
title = "Inductive Types"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b3"]
forwardlinks = ["3b3b"]
zettelid = "3b3a"
+++
CIC is built only on two straightforward features, function types and
inductive types, which can be used to reason about all theorems in math.
In Coq, implication and function types are actually the same thing, and
both therefore use the `->` operator. There is no overloading at play as
they are the same according to the Curry-Howard isomorphism.
Inductive and recursive types are the same because of the Curry-Howard
isomorphism, except for the `Prop` and `Set` distinction. Inductive
types would be easier to prove theorems with whereas recursive types
would actually be computable and can be extracted to OCaml code.
|
