You are close. Use MAP.
And please don’t use a mailing list to do assignments.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:49
To: hol-info
Subject: [Hol-info] assignment
The following data types are defined in HOL4.
val _ = Datatype `
Your problem statement doesn’t make sense. Why do you say “*the* ch in the
pop”? Surely a pop may contain multiple ch values.
As I said before, it seems as if you should try to write your program in SML
(or Haskell, or OCaml) first. Then you might think about formalising it in
HOL. If you wa
