1.前言
对lean4有兴趣纯意义，前面写过几篇文章介绍了如何快速安装和跑一个demo, 虽然有了初步结论lean4对如作者这样的工程狗是纯无用的东西。但是心中还是觉得缺点什么，一是结论可以草率，二是觉得应有妙处未体会。
下文从一个产BUG老能手的角度，用僵化的程序狗思路试再用一下lean4, 因为数学证明实在是太远，所以只能从程序入门角度试用。
其实我不知道别的程序员是怎么学一种新的编程语言，就自己而言一般是三个步骤：1. 搭个环境，跑个demo，2.最多花半天时间看一下基本语法，比如如何给变量赋值；3.等老板下命令就开玩，玩的过程就是全靠自己“执生”。
如果这个助跑时间超过两天的话，肯定有两天以上时间是在摸鱼。因为步骤1其实是可以花钱去某宝找人买环境的。
但是玩lean4真是掉坑里了，第一步就花了两天时间，因为没有人卖，干脆自己做了一个可以卖一键安装网盘包，也没空卖，还多花了一天两天时间写水文。第二步花了一周多看了一堆文章之后，只有一个结论：自己的脑子更合适擦地板而不是假装会写lean4代码。
2. [Lean4赋值语法及结构使用
先说初步的结论：
1. lean对类型异常敏感，甚至忽略了一般编程语言中的类型相容性处理，比如: int * float = float之类；
2. 程序出错也可以跑，很喜欢这种能冲就冲的风格，果然数学风格就是Open。
下面的代码就是一个测试的代码，用程序员习惯方式做一个lean 代码的demo, 目的只是让有程序基础的玩家做一个暖场的操作。把熟悉基础的时间压缩。
--import Mathlib.Tactic
--import Mathlib.Util.Delaborators
--import Mathlib.Data.Real.Basic
set_option diagnostics true
#eval "Hello, World!"
def s:String := "xxxx"
#check s
def b:Int := 2
def b2:Int := 2
#eval "============ b:Int := 2"
#eval b
def a:ℝ := 1.0
def c:UInt8 := 2
def d:UInt64 := 8989898
def de:UInt64 := 10
def h:Float := 20.0
def h1:Float := 40.0
#eval "============ a"
#eval a
#eval b
#eval c
#eval d
#eval a * b --会有结果：(sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/)
#eval d * de --898989810
#eval b * b2
#eval "============ b * d"
#eval b * d --会报错，类型不一致
#eval b * c * d
set_option diagnostics.threshold <num>
#eval "============ a * b * c * d"
#eval a * b * c * d
#eval "============ h"
#eval h
#eval h * h1
#eval h * b
#eval "============ U"
def e:Char := 'U'
#eval e
def o:ℕ := 0.5
#evalℕ * 0.6
--def f:Sort := 256
--#eval f
--对上述测试结果说明一点，lean 异常对类型敏感，甚至忽略了一般编程语言中的类型相容性处理，比如: int * float = float 之类
def s2:String := ":2xxxx"
#eval "============ s + s2"
#eval s + s2
--demo的方法有问题
--#check String.append("Hello, ", "Lean!")
--#eval String.append("Hello, ", "Lean!")
structure Point where
x : ℝ
y : ℝ
z : ℝ
def myPoint1 : Point where
x := 2
y := -1
z := 4
def myPoint2 : Point :=
⟨2, -1, 4⟩
#check Point
#check myPoint1
#check myPoint2
#eval "============ myPoint1 + myPoint1"
#eval myPoint1.x + myPoint2.x
#eval myPoint2.y + myPoint1.z
#eval myPoint2 + myPoint1
structure Int_Point where
x : Int
y : Int
z : Int
def myInt_Point1 : Int_Point :=
⟨2, -1, 4⟩
def myInt_Point2 : Int_Point :=
⟨3, 3, 3⟩
#eval "============ sInt_Point + Int_Point"
#eval myInt_Point1.x + myInt_Point2.x
#eval myInt_Point1.y + myInt_Point2.z
