Executable Specification

[View stlc.sig] [View stlc.mod]

sig stlc.

kind	tm, ty		type.

type 	i   		ty.
type	arrow 		ty -> ty -> ty.

type 	app 		tm -> tm -> tm.
type 	abs		ty -> (tm -> tm) -> tm.

type    tm              tm -> o.

module stlc.

tm (app M N) :- tm M, tm N.
tm (abs T R) :- pi x\ tm x => tm (R x).