Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 43 additions & 3 deletions src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts
Original file line number Diff line number Diff line change
@@ -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<string> {
const module = await leanSource()
return module.default
}

export default cauchySchwarzOq03Oq02Data