Search code examples
isabelle

Equivilant Haskell list comprehensions in Isabelle


The following List Comprehension in Haskell:

(i, 1) | i <- [7,7,7,8,8,8,2,2,1,1]

Will output the following tuples:

[(7,1),(7,1),(7,1),(8,1),(8,1),(8,1),(2,1),(2,1),(1,1),(1,1)]

What would be the equivalent code in Isabelle?


Solution

  • [(i, 1) . i <- [7,7,7,8,8,8,2,2,1,1]]
    

    which will be automatically translated to

    map (λi. (i, 1)) [7, 7, 7, 8, 8, 8, 2, 2, 1, 1]