 		}
 	}
 
-	public func withTypeParameters(recur: Recur, continuation: (Recur, [(String, Telescope<Recur>)]) -> Recur) -> Recur {
+	public func withTypeParameters(recur: Term, continuation: (Term, [(String, Telescope<Term>)]) -> Term) -> Term {
 		switch self {
 		case let .Argument(type, rest):
 			return type => { rest($0).withTypeParameters(.Application(recur, $0), continuation: continuation) }

//  Copyright © 2015 Rob Rix. All rights reserved.

public enum Datatype<Recur: TermType>: DictionaryLiteralConvertible {
	indirect case Argument(Recur, Recur -> Datatype)
	case End([(String, Telescope<Recur>)])


	public init(_ type: Recur, _ constructor: Recur -> Datatype<Recur>) {
		self = .Argument(type, constructor)
	}

	public init(_ type1: Recur, _ type2: Recur, _ constructor: (Recur, Recur) -> Datatype<Recur>) {
		self = .Argument(type1, { a in Datatype.Argument(type2) { b in constructor(a, b) } })
	}


	public init(dictionaryLiteral: (String, Telescope<Recur>)...) {
		self = .End(dictionaryLiteral)
	}


	public func definitions(recur: Recur, abstract: (Recur -> Recur) -> Recur -> Recur = { f in { f($0) } }) -> [(Name, Recur, Recur)] {
		switch self {
		case let .Argument(type, continuation):
			var parameter = Recur.Variable(.Local(-1))
			return continuation(Recur { parameter.out }).definitions(recur, abstract: { f in
				{ recur in
					Recur.lambda(type, {
						// We compute the continuation of the type constructor with respect to a parameter, but we need it to match up with the variable bound by this lambda at runtime. Since `TermType.self.lambda()` already implements the desired [circular programming](http://chris.eidhof.nl/posts/repmin-in-swift.html) behaviour, we can simply copy it out at this point and get the desired lazily-normalizing circular behaviour for the type constructor itself, instantiated correctly for each data constructor—even though they may have different numbers of parameters, and thus bind the type constructor’s parameter at a different variable.
						parameter = $0
						return f(.Application(recur, $0))

		}
	}

	public func value(symbol: String, telescope: Telescope<Term>, constructors: [(String, Telescope<Term>)], parameters: [Term] = [])(_ recur: Term) -> Term {
		switch telescope {
		case let .Recursive(rest):
			return recur => { self.value(symbol, telescope: rest, constructors: constructors, parameters: parameters + [ $0 ])(recur) }
