Mercurial > cpdt > repo

comparison src/DataStruct.v @ 572:a913f19955e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq 8.11
author Adam Chlipala <adam@chlipala.net>
date Sun, 02 Feb 2020 10:46:14 -0500
parents 0ce9829efa3b
children 1dc1d41620b6
comparison
equal deleted inserted replaced
571:3fc43e261f67 572:a913f19955e2
292 | Unit : type 292 | Unit : type
293 | Arrow : type -> type -> type. 293 | Arrow : type -> type -> type.
294 294
295 (** Now we can define a type family for expressions. An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts]. We effectively use the de Bruijn index variable representation%~\cite{DeBruijn}%. Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *) 295 (** Now we can define a type family for expressions. An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts]. We effectively use the de Bruijn index variable representation%~\cite{DeBruijn}%. Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
296 296
297 Inductive exp : list type -> type -> Set := 297 Inductive exp : list type -> type -> Type :=
298 | Const : forall ts, exp ts Unit 298 | Const : forall ts, exp ts Unit
299 (* begin thide *) 299 (* begin thide *)
300 | Var : forall ts t, member t ts -> exp ts t 300 | Var : forall ts t, member t ts -> exp ts t
301 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran 301 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
302 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran). 302 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).