49 lines
868 B
Plaintext
49 lines
868 B
Plaintext
/-
|
|
A generalization of `Lean.Name` that includes a file extension.
|
|
-/
|
|
import Lean
|
|
|
|
open Lean Name
|
|
|
|
inductive Extension where
|
|
| html
|
|
| pdf
|
|
deriving Repr
|
|
|
|
namespace Extension
|
|
|
|
def cmp : Extension → Extension → Ordering
|
|
| html, html => Ordering.eq
|
|
| html, _ => Ordering.lt
|
|
| pdf, pdf => Ordering.eq
|
|
| pdf, _ => Ordering.gt
|
|
|
|
instance : BEq Extension where
|
|
beq e1 e2 :=
|
|
match cmp e1 e2 with
|
|
| Ordering.eq => true
|
|
| _ => false
|
|
|
|
def toString : Extension → String
|
|
| html => "html"
|
|
| pdf => "pdf"
|
|
|
|
end Extension
|
|
|
|
structure NameExt where
|
|
name : Name
|
|
ext : Extension
|
|
|
|
namespace NameExt
|
|
|
|
def cmp (n₁ n₂ : NameExt) : Ordering :=
|
|
match Name.cmp n₁.name n₂.name with
|
|
| Ordering.eq => Extension.cmp n₁.ext n₂.ext
|
|
| ord => ord
|
|
|
|
def getString! : NameExt → String
|
|
| ⟨str _ s, _⟩ => s
|
|
| _ => unreachable!
|
|
|
|
end NameExt
|