Add some type annotations

Closes #1356 Closes #1357
HOL-Theorem-Prover · Nov 29, 2024 · 409fbbf · 409fbbf · binghe · Nov 30, 2024
1 parent 56f838f
commit 409fbbf
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
@@ -176,7 +176,7 @@ Definition LENGTH[simp]:
 End
 
 Definition MAP[simp]:
-  MAP f [] = [] /\
+  MAP (f:'a -> 'b) [] = [] /\
   MAP f (h::t) = f h::MAP f t
 End
 
@@ -234,8 +234,8 @@ End
 
 (* preserving particular variable quantification order *)
 Theorem EL:
-  (!l.    EL 0 l = HD l:'a) /\
-  (!l n.  EL (SUC n) l = EL n (TL l))
+  (!(l:'a list).    EL 0 l = HD l:'a) /\
+  (!(l:'a list) n.  EL (SUC n) l = EL n (TL l))
 Proof
   REWRITE_TAC[EL_def]
 QED