tweak lean link display

pi-base · Dec 6, 2023 · 03216d3 · 03216d3
1 parent d763464
commit 03216d3
Showing 1 changed file with 20 additions and 11 deletions.
diff --git a/packages/viewer/src/components/Properties/Show.svelte b/packages/viewer/src/components/Properties/Show.svelte
@@ -1,8 +1,17 @@
 <script lang="ts">
  import type { Property } from 'src/models'
- import { Aliases, References, Tabs, Title, Typeset } from '../Shared'
+ import {
+ Aliases,
+ Icons,
+ Link,
+ References,
+ Tabs,
+ Title,
+ Typeset,
+ } from '../Shared'
  import Spaces from './Spaces.svelte'
  import Theorems from './Theorems.svelte'
+ import Check from '../Shared/Icons/Check.svelte'
 
  export let property: Property
  export let tab: 'spaces' | 'theorems' | 'references'
@@ -26,19 +35,19 @@
 </h1>
 
 <section class="description">
+ {#if property?.lean}
+ <p>
+ <Icons.Robot />
+ <a href={leanUrl(property.lean)} target="_blank">
+ <code>{property.lean.id}</code>
+ in
+ <code>{property.lean.module}</code>
+ </a>
+ </p>
+ {/if}
  <Typeset body={property.description} />
 </section>
 
-{#if property?.lean}
- <section>
- <a href={leanUrl(property.lean)} target="_blank">
- Formalized in Lean as <code>{property.lean.id}</code>
- in
- <code>{property.lean.module}</code>
- </a>
- </section>
-{/if}
-
 <Tabs {tabs} {tab} {rel} />
 
 {#if tab === 'spaces'}