Random doc examples

Changes

2 changed files (+17/-0)

• palin.lean (new)
  • @@ -0,0 +1,8 @@
    + -- https://lean-lang.org/documentation/examples/palindromes/ + + inductive Palindrome : List Nat → Prop where + | nil : Palindrome [] + | single : (a : Nat) → Palindrome [a] + | sandwich : (a : Nat) → Palindrome as → Palindrome ([a] ++ as ++ [a]) + + #eval (Palindrome [3, 3])
• typedlambcalc.lean (new)
  • @@ -0,0 +1,9 @@
    + -- https://lean-lang.org/documentation/examples/phoas/ + + inductive Ty where + | nat + | fn : Ty → Ty → Ty + + @[reducible] def Ty.denote : Ty → Type + | nat => Nat + | fn a b => a.denote → b.denote