lean4-htt/tests/elab/cbv_annotations2.lean
Wojciech Różowski ccef9588ae
feat: add further cbv annotations (#13135)
This PR adds several `cbv_opaque` and `cbv_eval` annotations to the
standard library.
2026-03-26 14:55:40 +00:00

15 lines
455 B
Text

module
import Std
open Std
def isPalindrome (s : String) : Bool :=
s.chars.zip s.revChars |>.all (fun p => p.1 == p.2)
example : isPalindrome "" = true := by cbv
example : isPalindrome "aba" = true := by cbv
example : isPalindrome "aaaaa" = true := by cbv
example : isPalindrome "zbcd" = false := by cbv
example : isPalindrome "xywyx" = true := by cbv
example : isPalindrome "xywyz" = false := by cbv
example : isPalindrome "xywxz" = false := by cbv