Skip to content

Commit a52ce11

Browse files
committed
unified the two projects into one
1 parent c9500e9 commit a52ce11

15 files changed

Lines changed: 73 additions & 93 deletions

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11

22
**/*.DS_Store
3+
**/*~
34

45
/.lake

book/Fad.lean renamed to Book.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import VersoManual
22

3-
import Fad.FP
3+
import Book.FP
44

55
open Verso.Genre Manual
66
open Verso Code External

Fad/Chapter5.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -367,6 +367,11 @@ def subs (xs ys : List (a × Label)) : List (a × Pair) :=
367367
def switch : a × Pair → a × Pair
368368
| (x, (i, j)) => (-x, (j, i))
369369

370+
-- this need to be checked, added to fix error in `sortWith`
371+
instance : Ord (a × Pair) where
372+
compare p q :=
373+
compare p.1 q.1
374+
370375
def sortWith (abs : List (a × Pair)) (xis yis : List (a × Label))
371376
: List (a × Pair) :=
372377
let a := Std.HashMap.ofList (qsort₂ compare abs |>.map Prod.snd |>.zipIdx)

book/Main.lean renamed to MainBook.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import VersoManual
2-
import Fad
2+
import Book
33

44
open Verso.Genre Manual
55
open Verso Code External

book/.github/workflows/lean_action_ci.yml

Lines changed: 0 additions & 14 deletions
This file was deleted.

book/.gitignore

Lines changed: 0 additions & 3 deletions
This file was deleted.
File renamed without changes.

book/Fad/FP.lean renamed to book/FP.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import VersoManual
2-
import Fad.Basic
2+
import Book.Basic
33

44
open Verso.Genre Manual
55
open Fad

book/README.md

Lines changed: 0 additions & 1 deletion
This file was deleted.

book/lake-manifest.json

Lines changed: 0 additions & 35 deletions
This file was deleted.

0 commit comments

Comments
 (0)