We should kill Prop
Notação
Irei estar usando letras maiusculas para tipos e minusculas para o que não é um tipo ou é desconhecido.
Funções: (x : A) -> B
=== ∏x:A. B
, uma função que aceita x de um tipo A e retorna algo do tipo B, também chamado de abstração, a variável pode ser omitida quando ela não aparece em B A -> B
.
Implicito: {x : A} -> B
, uma função aonde o parametro é implicito, aka o compilador irá achar o argumento.
Módulo: (x : A, B)
=== Σx:A. B
, um módulo aonde a esquerda x tem um tipo A e a direita algo do tipo B, também chamado de par, módulos podem ser transparentes tendo a forma de (x : A = v, B
.