Add functions head and last to Cryptol prelude. Fixes #465.

Also fix regression test output.

lib/Cryptol.cry

@@ -522,6 +522,12 @@ drop ((_ : [front] _) # y) = y
 tail : {a, b} [1 + a]b -> [a]b
 tail xs = drop`{1} xs
 
+head : {a, b} [1 + a]b -> b
+head xs = xs @ 0
+
+last : {a, b} (fin a) => [1 + a]b -> b
+last xs = xs ! 0
+
 width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]
 width _ = `len
 

tests/issues/issue226.icry.stdout

@@ -78,11 +78,13 @@ Symbols
     groupBy :
       {each, parts, elem} (fin each) =>
         [each * parts]elem -> [parts][each]elem
+    head : {a, b} [1 + a]b -> b
     infFrom : {bits} (fin bits) => [bits] -> [inf][bits]
     infFromThen : {bits} (fin bits) => [bits] -> [bits] -> [inf][bits]
     integer : {val} (fin val) => Integer
     join :
       {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
+    last : {a, b} (fin a) => [1 + a]b -> b
     lg2 : {a} (Arith a) => a -> a
     max : {a} (Cmp a) => a -> a -> a
     min : {a} (Cmp a) => a -> a -> a

tests/issues/issue290v2.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    a`359 == 1
+    a`375 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11

tests/mono-binds/test04.icry.stdout

@@ -25,8 +25,8 @@ Loading module test04
 [error] at ./test04.cry:3:19--3:21:
   Type mismatch:
     Expected type: ()
-    Inferred type: [?j14]
+    Inferred type: [?z14]
   where
-  ?j14 is type parameter 'bits'
+  ?z14 is type parameter 'bits'
           of literal or demoted expression
           at ./test04.cry:3:19--3:21