rego-proofs/examples/04-rule-free-variables.prune.lean


1
2
3
4
5
6
7
8

-- Lean 4's syntax makes this quite nice...

def t2 : Option Bool :=
  let x := 42
  let y := 41
  if x > y then some true else none

-- Lift any local assignments and compile the rest to an ITE?