From 810eee3bc8dc2bfb251c15deeed8e9a9bb9436a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 24 Jun 2024 17:01:00 +0200 Subject: [PATCH] comment mathlib test --- tests/mathlib.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tests/mathlib.v b/tests/mathlib.v index 61a7857..191e153 100644 --- a/tests/mathlib.v +++ b/tests/mathlib.v @@ -3,3 +3,19 @@ From LeanImport Require Import Lean. Set Lean Error Mode "Stop". Time Redirect "mathlib.log" Lean Import "/home/gaetan/dev/lean/library/mathlib.out". + +(* +without hack first error at line 183121 (for int.div_zero) +with hack first error at line 210064 (for rat.one_mul) + *) + +Fail Check fun n d => fun x : + has_mul_mul_inst1 rat rat_has_mul + (rat_mk (has_one_one_inst1 int int_has_one) (has_one_one_inst1 int int_has_one)) + (rat_mk n (coe nat int (coe_to_lift nat int (coe_base nat int int_has_coe)) d)) = + rat_mk n (coe nat int (coe_to_lift nat int (coe_base nat int int_has_coe)) d) +=> +x : + has_mul_mul_inst1 rat rat_has_mul (has_one_one_inst1 rat rat_has_one) + (rat_mk n (coe nat int (coe_to_lift nat int (coe_base nat int int_has_coe)) d)) = + rat_mk n (coe nat int (coe_to_lift nat int (coe_base nat int int_has_coe)) d).