Lines Matching refs:nl
193 (`!gn i nl. (gn = GCODE i nl) ==> (GDECODE i gn = SOME nl)`,
198 `?h t. nl = h::t` by METIS_TAC [listTheory.list_CASES,GCODE_EQ_1] THEN
215 `!nl i. GDECODE i (GCODE i nl) = SOME nl`,
222 `!nl. DECODE (ENCODE nl) = nl`,
242 `!nl. gCONS n (ENCODE nl) = ENCODE (n::nl)`,
247 `!nl. gLEN (ENCODE nl) = LENGTH nl`,
257 `gMAP f (ENCODE nl) = ENCODE (MAP f nl)`,
262 `gFOLDL f a (ENCODE nl) = FOLDL f a nl`,
267 `gFOLDR f a (ENCODE nl) = FOLDR f a nl`,