Mercurial > cpdt > repo

comparison src/Intensional.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
187 (** %\vspace{-.15in}% [[ 187 (** %\vspace{-.15in}% [[
188 Wf = 188 Wf =
189 fun (t : type) (E : Exp t) => 189 fun (t : type) (E : Exp t) =>
190 forall var1 var2 : type -> Type, exp_equiv nil (E var1) (E var2) 190 forall var1 var2 : type -> Type, exp_equiv nil (E var1) (E var2)
191 : forall t : type, Exp t -> Prop 191 : forall t : type, Exp t -> Prop
192 ]] *) 192 ]]
193 *)
193 194
194 Section vars. 195 Section vars.
195 Variables var1 var2 : type -> Type. 196 Variables var1 var2 : type -> Type.
196 197
197 (** In the course of proving well-formedness, we will need to translate back and forth between the de Bruijn and PHOAS representations of free variable information. The function [zip] combines two de Bruijn substitutions into a single PHOAS context. *) 198 (** In the course of proving well-formedness, we will need to translate back and forth between the de Bruijn and PHOAS representations of free variable information. The function [zip] combines two de Bruijn substitutions into a single PHOAS context. *)