To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit 99edb424 authored by Alexander Soen's avatar Alexander Soen
Browse files

Add translate_interm tests

parent ed21b02d
open HolKernel Parse boolLib bossLib
open datatypeTranslateTheory
val _ = new_theory "datatypeTranslateTestsTheory"
val dict = ref (Binarymap.mkDict KernelSig.name_compare :
(KernelSig.kernelname, (hol_type * term)) Binarymap.dict)
val _ = insert_dict dict ((mk_kn "pred_set" "INSERT"),
(``:α -> (α -> bool) -> (α -> bool)``,
``CONS : α -> α list -> α list``))
val _ = insert_dict dict ((mk_kn "pred_set" "EMPTY"),
(``:α -> bool``,
``[] : α list``))
fun assert_translate_interm dict init_tm assert_tm =
let
val fin_tm = translate_interm (! dict) init_tm
in
prove (mk_eq (fin_tm, assert_tm), simp[])
end
val _ = assert_translate dict ``{}:'a -> bool`` ``[]:'a list``
val _ = assert_translate dict ``{x:num}`` ``[x:num]``
val _ = assert_translate dict ``{ODD}`` ``[ODD]:(num -> bool) list``
val _ = assert_translate dict ``{{}:'a -> bool}`` ``[[]:'a list]``
val _ = assert_translate dict ``{{}; x:num}`` ``[[]; x:num]``
val _ = assert_translate dict ``{}:'a -> bool=y`` ``[]:'a list=y``
val _ = assert_translate dict ``[{3}]`` ``[[3]]``
val _ = export_theory ()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment