Twelf(Q) Architecture

• Unification is seen as a constraint solving module

• There are possibly many other modules

• Constraints of these other modules are expressed as predicates (type families):

  > : rational -> rational -> type.
  
  ...

Previous slide

Next slide

Back to first slide

View graphic version