From aa2b2dbabae7e9698bcc2ed0278b8189223ac136 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Mon, 4 Dec 2023 16:01:12 -0500
Subject: [PATCH] clean up ML module

---
 SciLean/Modules/ML/DenseLayer.lean | 21 ---------------------
 1 file changed, 21 deletions(-)
 delete mode 100644 SciLean/Modules/ML/DenseLayer.lean

diff --git a/SciLean/Modules/ML/DenseLayer.lean b/SciLean/Modules/ML/DenseLayer.lean
deleted file mode 100644
index abe88d78..00000000
--- a/SciLean/Modules/ML/DenseLayer.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import SciLean
-import SciLean.Core.Meta.GenerateRevCDeriv'
-
-namespace SciLean.ML
-
-variable 
-  {K : Type} [RealScalar K]
-  {W : Type} [Vec K W]
-
-set_default_scalar K
-
-variable {α β κ ι : Type} [Index κ] [Index ι] [PlainDataType K] [PlainDataType R]
-
-variable (κ)
-def dense (weights : K^(κ×ι)) (bias : K^κ) (x : K^ι) : K^κ := 
-  ⊞ j => ∑ i, weights[(j,i)] * x[i] + bias[j]
-variable {κ}
-
-#generate_revDeriv dense weights bias x
-  prop_by unfold dense; fprop
-  trans_by unfold dense; ftrans