Commit788f95e

committed

Merge pull request#2 from MatthewFluet/array-type-str-resp-eq

Add array special case to defn of type structure respects equality

2 parents2787e0a +37e6ac9 commit788f95eCopy full SHA for 788f95e

File tree

-1

lines changed

-1

lines changed

23 Bytes

Binary file not shown.

Lines changed: 1 addition & 1 deletion

Original file line number	Diff line number	Diff line change
`@@ -503,7 +503,7 @@ \subsection{Type Structures and Type Environments}`
`503`	`503`
`504`	`504`	`A type structure\replacement{\thece}{$(\t,\CE)$}{$(\t,\VE)$}\is said to`
`505`	`505`	`{\sl respect equality} if, whenever$\t$ admits equality, then`
`506`		`-either$\t=\REF$ (see Appendix~\ref{init-stat-bas-app}) or,`
	`506`	`+either$\t=\REF$\ADD{or$\t=\ARRAY$}(see Appendix~\ref{init-stat-bas-app}) or,`
`507`	`507`	`for each\replacement{\theidstatus}{$\CE(\con)$}{$\VE(\vid)$} of the form`
`508`	`508`	`\replacement{\thece}{$\forall\alphak.(\tau\rightarrow\alphak\t)$,}{$(\forall\alphak.(\tau\rightarrow\alphak\t),\is)$,}`
`509`	`509`	`the type function$\Lambda\alphak.\tau$ also admits equality.`

Comments

(0)