isabelle: src/Pure/term.scala@753eb5b83370 (annotated)

43730 a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	1	/* Title: Pure/term.scala
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	2	Author: Makarius
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	3
43779 47bec02c6762 more uniform Term and Term_XML modules; wenzelm parents: 43778 diff changeset	4	Lambda terms, types, sorts.
43730 a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	5
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	6	Note: Isabelle/ML is the primary environment for logical operations.
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	7	*/
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	8
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	9	package isabelle
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	10
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	11
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	12	object Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	13	{
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	14	type Indexname = (String, Int)
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	15
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	16	type Sort = List[String]
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	17	val dummyS: Sort = List("")
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	18
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	19	sealed abstract class Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	20	case class Type(name: String, args: List[Typ] = Nil) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	21	case class TFree(name: String, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	22	case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	23	val dummyT = Type("dummy")
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	24
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	25	sealed abstract class Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	26	case class Const(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	27	case class Free(name: String, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	28	case class Var(name: Indexname, typ: Typ = dummyT) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	29	case class Bound(index: Int) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	30	case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
a0ed7bc688b5 lambda terms with XML data representation in Scala; wenzelm parents: diff changeset	31	case class App(fun: Term, arg: Term) extends Term
43731 70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); wenzelm parents: 43730 diff changeset	32	}
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); wenzelm parents: 43730 diff changeset	33

author	wenzelm
	Tue, 08 Aug 2017 11:49:35 +0200
changeset 66377	753eb5b83370
parent 43779	47bec02c6762
child 68265	f0899dad4877
permissions	-rw-r--r--