+assoc' y x (x * y) 换成 sym ( +assoc y x (x * y) )
乘法结合律精简的证明：
*-assoc : (x y z : ?) → (x * y) * z ≡ x * (y * z)*-assoc zero y z = refl*-assoc (suc x) y z rewrite *distribr y (x * y) z | *-assoc x y z = refl一些比较大小n≮n : (n : ?) → n < n ≡ falsen≮n zero = refln≮n (suc x) = n≮n x-- problem 2.2<-antisym : (x y : ?) → x < y ≡ true → y < x ≡ false<-antisym zero (suc y) p1 = refl<-antisym (suc x) (suc y) = <-antisym x y -- problem 2.3<-trichotomy : (x y : ?) → x < y ∨ x =? y ∨ y < x ≡ true<-trichotomy zero zero = refl<-trichotomy zero (suc y) = refl<-trichotomy (suc x) zero = refl<-trichotomy (suc x) (suc y) = <-trichotomy x y【Agda学习笔记1】
推荐阅读
- 萌新版 xss学习笔记
- 1 JAVA语言学习-面向对象
- MyBatis笔记03------XXXMapper.xml文件解析
- 一百二十 salesforce零基础学习快去迁移你的代码中的 Alert / Confirm 以及 Prompt吧
- 我的Spark学习笔记
- 7000-8000高性价比笔记本排行榜2022-7000-8000值得买的笔记本排行榜
- JVM学习笔记——垃圾回收篇
- 黑莓q5用安装微信的方法a 用黑莓自带的印象笔记手敲的 看不懂的宝宝们在私聊我吧
- JVM学习笔记——内存结构篇
- 【lwip】08-ARP协议一图笔记及源码实现