wenzelm@51397: chapter CTT wenzelm@51397: wenzelm@48738: session CTT = Pure + wenzelm@48475: description {* wenzelm@48475: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@48475: Copyright 1991 University of Cambridge wenzelm@51403: wenzelm@51403: This is a version of Constructive Type Theory (extensional equality, wenzelm@51403: no universes). wenzelm@51403: wenzelm@51403: Useful references on Constructive Type Theory: wenzelm@51403: wenzelm@51403: B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's wenzelm@51403: Type Theory (Oxford University Press, 1990) wenzelm@51403: wenzelm@51403: Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, wenzelm@51403: 1991) wenzelm@48475: *} wenzelm@48483: options [document = false] wenzelm@48475: theories Main wenzelm@48475: wenzelm@48738: session "CTT-ex" in ex = CTT + wenzelm@48475: description {* wenzelm@48475: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@48475: Copyright 1991 University of Cambridge wenzelm@48475: wenzelm@48475: Examples for Constructive Type Theory. wenzelm@48475: *} wenzelm@48483: options [document = false] wenzelm@48475: theories Typechecking Elimination Equality Synthesis