Agda (Rev #3, changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

Agda is a proof assistant based on MLTT with a countable hierarchy of explicitly polymorphic universes, very powerful inductive-inductive types? and ~~inductive-recursive types?~~inductive-recursive types, and a flexible pattern-matching? syntax.

Agda’s default pattern-matching rules are incompatible with the univalence axiom; they allow one to prove axiom K?. However, there is a flag which restricts them so that they are guaranteed to be expressible in terms of the induction principle without using K. Current versions of Agda use a syntactic check for this, which contains errors, but it has been shown that a modification of the the algorithm yields a correct restriction.