From 537c403d3efcf9b36897809a40cc7f5c1a871507 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 26 Dec 2018 19:20:21 +0100 Subject: [PATCH] automatically inserted aliases --- matita/matita/broken_lib/reverse_complexity/hierarchy.ma | 2 ++ 1 file changed, 2 insertions(+) diff --git a/matita/matita/broken_lib/reverse_complexity/hierarchy.ma b/matita/matita/broken_lib/reverse_complexity/hierarchy.ma index a621b55a5..f288e98ca 100644 --- a/matita/matita/broken_lib/reverse_complexity/hierarchy.ma +++ b/matita/matita/broken_lib/reverse_complexity/hierarchy.ma @@ -46,6 +46,8 @@ lemma Max0r : ∀n. max n 0 = n. #n >commutative_max // qed. +alias id "max" = "cic:/matita/arithmetics/nat/max#def:2". +alias id "mk_Aop" = "cic:/matita/arithmetics/bigops/Aop#con:0:1:2". definition MaxA ≝ mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)). -- 2.39.2