SeLFiE: some supports to reason goals with if-then-else.

data61 / PSL

Other

65 stars 9 forks source link

Closed yutakang closed 4 years ago

yutakang commented 4 years ago

@{term "if x then y else z"};
(*
  Const ("HOL.If", "bool ⇒ 'a ⇒ 'a ⇒ 'a") 
$ Free ("x", "bool") 
$ Free ("y", "'a") 
$ Free ("z", "'a"): term
*)

yutakang commented 4 years ago

We would like to have something like With_If_Then_Else (x, y, z).

yutakang commented 4 years ago

I introduced Is_If_Then_Else (x, y, z) because I think only quantifiers should bind variables.

Done in 2de085e35be389f6449e26663b46155279d46930.