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


1
2
3
4
5
6
7
8
9
10
11
12
13
14

inductive t2_eqv (rhs : Rego.Any) : Prop
| rule₁ : (let x := 42
           let y := 41
           x > y) →
          (rhs = Rego.Any.bool true) →
          t2_eqv rhs

-- Alternative form where the parameters are unnamed.

inductive t2_eqv' : Bool → Prop
| rule₁ : (let x := 42
           let y := 41
           x > y) →
          t2_eqv' true