From 86cb5cbdfe8ef66a1f2fc416805aede25b78cec2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Oct 2020 09:46:38 -0700 Subject: [PATCH] chore: remove auxiliary definition for old frontend --- src/Init/Core.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 739fb3dd6d..5bd57fbfe0 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -41,10 +41,6 @@ theorems generated by the equation Compiler. /-- Auxiliary Declaration used to implement the notation (a : α) -/ @[reducible] def typedExpr (α : Sort u) (a : α) : α := a -/- `idRhs` is an auxiliary Declaration used in the equation Compiler to address performance - issues when proving equational theorems. The equation Compiler uses it as a marker. -/ -@[macroInline, reducible] def idRhs (α : Sort u) (a : α) : α := a - /-- Auxiliary Declaration used to implement the named patterns `x@p` -/ @[reducible] def namedPattern {α : Sort u} (x a : α) : α := a