Lean - Dependent Type
Posted on August 2, 2019
Tags: lean
1 Dependent Product
1.1 Type Formation
\[\cfrac{\vdash X:Type \qquad x:X \vdash A(x):Type}{\vdash \prod\limits_{x:X} A(x) : Type }\]
1.2 Term Introduction
\[\cfrac{ x:X \vdash a(x):A(X)}{\vdash \lambda x. a(x) : \prod\limits_{x':X} A(x') }\]
2 Reading inductive types
inductive score : Type :=
| A : score
| B : score
| C : score
inductive Step : Score -> Score -> Prop :=
| * :.. -> Step A B
| % :.. -> Step B C
| o :.. -> Step A C Type Formation +----------------------------+
| Prop |
| |
| |
+--------------+ +--------------+ | +---------+ |
| Type | | Type | | |Step A B | |
| | | | | | | +--------+ |
| | | | | | + | |Step B C| |
| +----------+ | | +----------+ | | | * | | | |
| | Score | | | | Score | | | | & | | % | |
| | C | | | | B | | | +---------+ | | |
| |A --------------> A ---------------> | + | |
| | B | | | | C | | | | ^ | |
| +----------+ | | +----------+ | | +----------+ | | |
| | | | | | Step A C | +--------+ |
+--------------+ +--------------+ | | | |
| | * o | |
| +----------+ |
| |
+----------------------------+Term introduction is us selecting one of those terms * + ^ inside a Step _ _ set
