tests/elab/9089.lean - third_party/github.com/leanprover/lean4 - Git at Google


          
            
            example : ((let f := @Bool.rec (fun _ => Bool × Unit) (false, ()) (true, ()); f) true).1 = true := rfl