Skip to content
Experiments in dependent type support for Isabelle
Standard ML Isabelle OCaml
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitignore ROOT Oct 8, 2019
Elaboration.thy
Identity.thy
README.md
ROOT variable prep functions working properly now, I think Oct 15, 2019
Spartan.thy
elaboration.ML Back to deeply-embedded universe constants and explicit level annotat… Nov 7, 2019
equality.ML
implicits.ML small reorganization Oct 15, 2019
lib.ML
schematic_subgoal.ML
subtyping.ML

README.md

Dependent types for Isabelle

Experiments in dependent type theory support in Isabelle.

  • Current work is focused on:

    • Term elaboration
    • The universe hierarchy
    • Better Isar integration with identity type reasoning — commit 90121d4
  • You may also be interested in homotopy type theory in Isabelle, which this project aims to improve on.

  • Why "spartan"?

You can’t perform that action at this time.