 //  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 enum Datatype<Term: TermType>: DictionaryLiteralConvertible {
+	indirect case Argument(Term, Term -> Datatype)
+	case End([(String, Telescope<Term>)])
 
 
-	public init(_ type: Recur, _ constructor: Recur -> Datatype<Recur>) {
+	public init(_ type: Term, _ constructor: Term -> Datatype<Term>) {
 		self = .Argument(type, constructor)
 	}
 
-	public init(_ type1: Recur, _ type2: Recur, _ constructor: (Recur, Recur) -> Datatype<Recur>) {
+	public init(_ type1: Term, _ type2: Term, _ constructor: (Term, Term) -> Datatype<Term>) {
 		self = .Argument(type1, { a in Datatype.Argument(type2) { b in constructor(a, b) } })
 	}
 
 
-	public init(dictionaryLiteral: (String, Telescope<Recur>)...) {
+	public init(dictionaryLiteral: (String, Telescope<Term>)...) {
 		self = .End(dictionaryLiteral)
 	}
 
 
-	public func definitions(recur: Recur, abstract: (Recur -> Recur) -> Recur -> Recur = { f in { f($0) } }) -> [(Name, Recur, Recur)] {
+	public func definitions(recur: Term, abstract: (Term -> Term) -> Term -> Term = { f in { f($0) } }) -> [(Name, Term, Term)] {
 		switch self {
 		case let .Argument(type, continuation):
-			var parameter = Recur.Variable(.Local(-1))
-			return continuation(Recur { parameter.out }).definitions(recur, abstract: { f in
+			var parameter = Term.Variable(.Local(-1))
+			return continuation(Term { parameter.out }).definitions(recur, abstract: { f in
 				{ recur in
-					Recur.lambda(type, {
+					Term.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))

			} >>> abstract)
		case let .End(constructors):
			return constructors.map {
				// Since at this point the type and value both close over the same parameter despite its inevitable use at two different indices, we copy them recursively using `Recur(term:)` to ensure that they’re finished with the shared state by the time they’re returned to the caller.
				(.Global($0), Recur(term: abstract(self.type($1))(recur)), Recur(term: abstract(self.value($0, telescope: $1, constructors: constructors))(recur)))
			}
		}
	}

	public func type(telescope: Telescope<Recur>)(_ recur: Recur) -> Recur {
		switch telescope {
		case let .Recursive(rest):
			return recur --> type(rest)(recur)

		}
	}

	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) }
