Istari

The Istari Library

The Core library

The following libraries are pre-loaded:

• Acc (accessibility)
• Bar (simulated partial computable objects)
• Bool
• Decidable
• Finite
• FiniteMap
• Function
• Integer
• Irrelevance (proof irrelevance)
• Kindlike (types eligible for impredicative quantification)
• Logic
• List
• Misc
• Nat
• Natural (natural numbers using “native” arithmetic)
• Option
• Partial (partial computable objects)
• Permutation (permutations on lists)
• Quotient (tools for manipulating quotient types)
• Relations
• Stable
• Symbol
• Tuple
• Weaksum (an improved interface for union types)
• Wtype (well-founded types)

Other libraries

The following libraries can be loaded from the library directory:

• GirardParadox (type is not a type)
• SmithParadox (there exist inadmissible types)

This site is open source. Improve this page.