We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 46ea63e commit f18f45aCopy full SHA for f18f45a
examples/divScript.sml
@@ -318,8 +318,8 @@ QED
318
(* TODO: Move REPLICATE_LIST and lemmas to an appropriate theory *)
319
320
val REPLICATE_LIST_def = Define `
321
- (!l. REPLICATE_LIST l 0 = []) /\
322
- (!l n. REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
+ (REPLICATE_LIST l 0 = []) /\
+ (REPLICATE_LIST l (SUC n) = REPLICATE_LIST l n ++ l)`
323
324
Theorem REPLICATE_LIST_SNOC:
325
!x n. SNOC x (REPLICATE_LIST [x] n) = REPLICATE_LIST [x] (SUC n)
0 commit comments