localrw.fq

fixpoint "--localrewrites"
fixpoint "--rewrite"
fixpoint "--allowho"

bind 1 g : { V : Int | true }
bind 2 g : { V : Int | true }

defineLocal 1 [g := (40 + 1)]

expand [1 : True]

constraint:
    env [2]
    lhs { V : Tuple | true }
    rhs { V : Tuple | (g = 41) }
    id 1 tag []