2 lines
514 B
Text
2 lines
514 B
Text
{"seq_num":0,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\nparameter [decidable_eq nat]\n\nend s1\n"}
|
|
{"seq_num":2,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\n\nparameter [decidable_eq nat]\n\nend s1\n"}
|