   ///
   /// The signature of the function is not immediately available, but may be
   /// acquired by querying the context with the qualified name.
-  case function(QualifiedName, [Clause])
+  case function(QualifiedName, [DeclaredClause])
   /// The body of a data declaration.
   ///
   /// E.g. this portion of the standard definition of

  case function(Expr, Expr)
  /// A lambda binding some variables of the same type to some output expression
  /// that may depend on those variables.
  case lambda(([Name], Expr), Expr)
  /// A type constructor for a term.
  case constructor(QualifiedName, [Expr])
  /// The "Type" sort.

      return false
    }
  }

  public var description: String {
    switch self {
    case .refl:
      return "refl"
    case .type:
      return "Type"
    case let .pi(name, .pi(iname, llhs, lrhs), rhs):
      return "(\(name) : (\(iname) : \(llhs) -> \(lrhs))) -> \(rhs)"
    case let .pi(name, lhs, rhs):
      return "(\(name) : \(lhs)) -> \(rhs)"
    case let .function(.function(llhs, lrhs), rhs):
      return "(\(llhs) -> \(lrhs)) -> \(rhs)"
    case let .function(lhs, rhs):
      return "\(lhs) -> \(rhs)"
    case .meta:
      return "$META"
    case let .lambda(body):
      return "λ . \(body)"
    case let .equal(eqTy, lhs, rhs):
      return "\(lhs) =(\(eqTy))= \(rhs)"
    case let .constructor(openTm, args):
      return "\(openTm)(\(args.map({$0.description}).joined(separator: ", ")))"
    case let .apply(head, elims):
      switch head {
      case let .definition(def):
        guard !elims.isEmpty else { return "\(def)" }
        return "\(def)[\(elims.map({$0.description}).joined(separator: ", "))]"
      case let .variable(vari):
        guard !elims.isEmpty else { return "\(vari)" }
        return "\(vari)[\(elims.map({$0.description}).joined(separator: ", "))]"
      }
    }
  }
}

/// Represents the "head" of an application expression.
