文件名称：Records:具有原型继承的相关类型可扩展记录
文件大小：2KB
文件格式：ZIP
更新时间：2024-07-13 12:05:34
Idris
具有原型继承的相关类型可扩展记录 具有强大正确性保证的“动态”记录系统。 创造 test : Record {lbl=String} ?testTy test = [ " foo " := 1 , " bar " := " a thing " , " bleh " := 1.2 ] testTy = proof search 添加 test2 : ?test2Ty test2 = ( " meh " := 10 ) :: test test2Ty = proof search 去掉 test3 : ?test3Ty test3 = getProof $ " meh " - test test3Ty = proof search 更新 test4 : ?test4Ty test4 = getProof $ ( " meh " := 11 ) -: test
【文件预览】：
Records-master
----Record.idr(2KB)
----Readme.md(899B)