diff --git a/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts b/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts index b98fd7b6df1..1e16449b2cc 100644 --- a/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts +++ b/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts @@ -1,4 +1,44 @@ -import meta from "./meta.json"; -import annotations from "./annotations.json"; +import type { Proof, Annotation, ProofData, ProofMeta, ProofSection, ProofOverview, ProofConclusion, CrossReference } from '@/types/proof' +import metaJson from './meta.json' +import annotationsJson from './annotations.json' -export { meta, annotations }; +const meta = metaJson as unknown as { + id: string + title: string + slug: string + description: string + meta: ProofMeta + sections: ProofSection[] + overview?: ProofOverview + conclusion?: ProofConclusion + crossReferences?: CrossReference[] +} + +const leanSource = () => import('../../../../proofs/Proofs/CauchySchwarzOQ03OQ02.lean?raw') + +export const cauchySchwarzOq03Oq02Proof: Proof = { + id: meta.id, + title: meta.title, + slug: meta.slug, + description: meta.description, + meta: meta.meta, + sections: meta.sections, + source: '', + overview: meta.overview, + conclusion: meta.conclusion, + crossReferences: meta.crossReferences, +} + +export const cauchySchwarzOq03Oq02Annotations: Annotation[] = annotationsJson as unknown as Annotation[] + +export const cauchySchwarzOq03Oq02Data: ProofData = { + proof: cauchySchwarzOq03Oq02Proof, + annotations: cauchySchwarzOq03Oq02Annotations, +} + +export async function getProofSource(): Promise { + const module = await leanSource() + return module.default +} + +export default cauchySchwarzOq03Oq02Data