LAURENT

ANALYTICAL TYPE SYSTEM

MLTT

  1. PROP
  2. U0 : U1
  3. FORALL
  4. EXISTS
  5. AND
  6. OR
  7. REAL

SET

  1. SET
  2. EQZ3
  3. \
  4. INTERSECT
  5. CLOSURE
  6. POWER

MU

  1. MU
  2. MEASURE
  3. LEBESGUE

CALC

  1. SEQ
  2. INF
  3. SUP
  4. LIMIT
  5. SUM
  6. UNION


.

$ git clone \ [email protected]:groupoid/laurent $ opam install z3 $ ocamlfind ocamlc -o laurent \ -package z3 -linkpkg src/laurent.ml

SYNTAX

SEMANTICS


MLTT

(-Formation, Dependent Product). -types represents the way we create the spaces of dependent functions with domain in and codomain in type family over .

(-Formation, Dependent Sum). The dependent sum type is indexed over type in the sense of coproduct or disjoint union, where only one fiber codomain is present in pair.


🧊


Присвячується Володимиру Олександровичу Клименку. Механізована верифікація теорем функціонального аналізу і теорії розподілів Лорана Шварца.