Extraction to Haskell Int type


I am trying to extract my project into Haskell. I have a type that handles memory addresses which I want to extract to Haskell Int (instead of Integer).
Which standard library numeric type should I use for this?

1 Like

It seems to me that you are looking for the Extract Constant command

Here you can find a more detailed explanation of how to properly extract your programs

Use the following (add more as necessary)

Require Import Extraction.
Extraction Language Haskell.

Extract Inductive list => "[]" [ "[]" "(:)" ].
Extract Inductive prod => "(,)"  [ "(,)" ].
Extract Inductive sum => "Prelude.Either"  [ "Prelude.Left" "Prelude.Right" ].
Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ] "(\fO fS n -> if n Prelude.== 0 then fO () else fS (Prelude.pred n))".

Extract Constant plus => "(Prelude.+)".
Extract Constant andb => "(Prelude.&&)".
Extract Constant fst => "Prelude.fst".
Extract Constant snd => "Prelude.snd".