Skip to content

Instantly share code, notes, and snippets.

@ice1000

ice1000/aya-trace-wow.md

Last active August 26, 2022 20:37
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ice1000/2575e568355e157b19874830502b1b42 to your computer and use it in GitHub Desktop.
Save ice1000/2575e568355e157b19874830502b1b42 to your computer and use it in GitHub Desktop.
Download ZIP
Trace generated by Aya checking wow.aya
Raw
aya-trace-wow.md
  • telescope of Nat
    • ⊢ Type
      • result ⊢ Type ↑ Type
  • telescope of zero
  • zero
  • telescope of Nat
    • ⊢ Type
      • result ⊢ Type ↑ Type
  • telescope of suc
    • ⊢ Nat : Type
      • ⊢ Nat
        • result ⊢ Nat ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ Nat ↑ Type
  • Nat
    • zero
      • zero
    • suc
      • suc
  • suc
  • telescope of Unit
    • ⊢ Type
      • result ⊢ Type ↑ Type
  • telescope of unit
  • unit
  • Unit
    • unit
      • unit
  • telescope of wow-fun
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ U -> Type
      • ⊢ U
        • result ⊢ U ↑ Type
      • ⊢ Type
        • result ⊢ Type ↑ Type
      • result ⊢ U -> Type ↑ Type
    • ⊢ U
      • result ⊢ U ↑ Type
    • ⊢ U
      • result ⊢ U ↑ Type
    • ⊢ T A
      • ⊢ T
        • result ⊢ T ↑ U -> Type
      • ⊢ A : U
        • ⊢ A
          • result ⊢ A ↑ U
        • ⊢ U ≡ U
        • ⊢ U ≡ U
        • result ⊢ A ↑ U
      • result ⊢ T A ↑ Type
    • ⊢ T B
      • ⊢ T
        • result ⊢ T ↑ U -> Type
      • ⊢ B : U
        • ⊢ B
          • result ⊢ B ↑ U
        • ⊢ U ≡ U
        • ⊢ U ≡ U
        • result ⊢ B ↑ U
      • result ⊢ T B ↑ Type
    • ⊢ Nat
      • result ⊢ Nat ↑ Type
  • wow-fun
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ U -> Type
      • ⊢ U
        • result ⊢ U ↑ Type
      • ⊢ Type
        • result ⊢ Type ↑ Type
      • result ⊢ U -> Type ↑ Type
    • ⊢ U
      • result ⊢ U ↑ Type
    • ⊢ U
      • result ⊢ U ↑ Type
    • ⊢ T A
      • ⊢ T
        • result ⊢ T ↑ U -> Type
      • ⊢ A : U
        • ⊢ A
          • result ⊢ A ↑ U
        • ⊢ U ≡ U
        • ⊢ U ≡ U
        • result ⊢ A ↑ U
      • result ⊢ T A ↑ Type
    • ⊢ T B
      • ⊢ T
        • result ⊢ T ↑ U -> Type
      • ⊢ B : U
        • ⊢ B
          • result ⊢ B ↑ U
        • ⊢ U ≡ U
        • ⊢ U ≡ U
        • result ⊢ B ↑ U
      • result ⊢ T B ↑ Type
    • ⊢ Nat
      • result ⊢ Nat ↑ Type
    • ⊢ zero : Nat
      • ⊢ zero
        • result ⊢ zero ↑ Nat
      • ⊢ Nat ≡ Nat
      • ⊢ Nat ≡ Nat
      • result ⊢ zero ↑ Nat
  • telescope of Wow
    • ⊢ Type
      • result ⊢ Type ↑ Type
  • telescope of wow
    • ⊢ Type : Type
      • result ⊢ Type ↑ Type
    • ⊢ U -> Type : Type
      • ⊢ U -> Type
        • ⊢ U
          • result ⊢ U ↑ Type
        • ⊢ Type
          • result ⊢ Type ↑ Type
        • result ⊢ U -> Type ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ U -> Type ↑ Type
    • ⊢ U : Type
      • ⊢ U
        • result ⊢ U ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ U ↑ Type
    • ⊢ U : Type
      • ⊢ U
        • result ⊢ U ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ U ↑ Type
    • ⊢ T A : Type
      • ⊢ T A
        • ⊢ T
          • result ⊢ T ↑ U -> Type
        • ⊢ A : U
          • ⊢ A
            • result ⊢ A ↑ U
          • ⊢ U ≡ U
          • ⊢ U ≡ U
          • result ⊢ A ↑ U
        • result ⊢ T A ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ T A ↑ Type
    • ⊢ T B : Type
      • ⊢ T B
        • ⊢ T
          • result ⊢ T ↑ U -> Type
        • ⊢ B : U
          • ⊢ B
            • result ⊢ B ↑ U
          • ⊢ U ≡ U
          • ⊢ U ≡ U
          • result ⊢ B ↑ U
        • result ⊢ T B ↑ Type
      • ⊢ Type ≡ Type
      • ⊢ Type ≡ Type
      • result ⊢ T B ↑ Type
  • wow
  • Wow
    • wow
      • wow
  • ⊢ wow
    • result ⊢ wow ↑ Pi {U : Type} {T : U -> Type} (A B : U) (T A) (T B) -> Wow
  • telescope of test1
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ A
      • result ⊢ A ↑ Type
    • ⊢ B
      • result ⊢ B ↑ Type
    • ⊢ _
      • ⊢ _ : _8
        • result ⊢ _8 ↑ _8
      • result ⊢ _8 ↑ _8
  • test1
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ A
      • result ⊢ A ↑ Type
    • ⊢ B
      • result ⊢ B ↑ Type
    • ⊢ _
      • ⊢ _ : _8
        • result ⊢ _8 ↑ _8
      • result ⊢ _8 ↑ _8
    • ⊢ wow A B a b : _8
      • ⊢ wow A B a b
        • ⊢ wow A B a
          • ⊢ wow A B
            • ⊢ wow A
              • ⊢ wow
                • result ⊢ wow ↑ Pi {U : Type} {T : U -> Type} (A B : U) (T A) (T B) -> Wow
              • ⊢ A : U'
                • ⊢ A
                  • result ⊢ A ↑ Type
                • ⊢ Type ≡ U'
                • ⊢ U' ≡ Type
                  • ⊢ Type ≡ Type
                  • Hole solved!
                • result ⊢ A ↑ Type
              • result ⊢ wow A ↑ Pi (B : Type) (T' A) (T' B) -> Wow
            • ⊢ B : Type
              • ⊢ B
                • result ⊢ B ↑ Type
              • ⊢ Type ≡ U'
              • ⊢ Type ≡ Type
              • result ⊢ B ↑ Type
            • result ⊢ wow A B ↑ T' A -> T' B -> Wow
          • ⊢ a : T' A
            • ⊢ a
              • result ⊢ a ↑ A
            • ⊢ A ≡ T' A
            • ⊢ T' A ≡ A
              • ⊢ Type ≡ Type
              • Hole solved!
            • result ⊢ a ↑ A
          • result ⊢ wow A B a ↑ _7 -> Wow
        • ⊢ b : _7
          • ⊢ b
            • result ⊢ b ↑ B
          • ⊢ B ≡ T' B
          • ⊢ B ≡ B
          • result ⊢ b ↑ B
        • result ⊢ wow A B a b ↑ Wow
      • ⊢ Wow ≡ _8
      • ⊢ _8 ≡ Wow
        • ⊢ Type ≡ _8
        • Hole solved!
      • result ⊢ wow A B a b ↑ Wow
  • ⊢ test1
    • result ⊢ test1 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test1
    • result ⊢ test1 ↑ Pi {A B : Type} {A} {B} -> Wow
  • telescope of test2
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ A
      • result ⊢ A ↑ Type
    • ⊢ B
      • result ⊢ B ↑ Type
    • ⊢ _
      • ⊢ _ : _6
        • result ⊢ _6 ↑ _6
      • result ⊢ _6 ↑ _6
  • test2
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ Type
      • result ⊢ Type ↑ Type
    • ⊢ A
      • result ⊢ A ↑ Type
    • ⊢ B
      • result ⊢ B ↑ Type
    • ⊢ _
      • ⊢ _ : _6
        • result ⊢ _6 ↑ _6
      • result ⊢ _6 ↑ _6
    • ⊢ wow A B a a : _6
      • ⊢ wow A B a a
        • ⊢ wow A B a
          • ⊢ wow A B
            • ⊢ wow A
              • ⊢ wow
                • result ⊢ wow ↑ Pi {U : Type} {T : U -> Type} (A B : U) (T A) (T B) -> Wow
              • ⊢ A : U'
                • ⊢ A
                  • result ⊢ A ↑ Type
                • ⊢ Type ≡ U'
                • ⊢ U' ≡ Type
                  • ⊢ Type ≡ Type
                  • Hole solved!
                • result ⊢ A ↑ Type
              • result ⊢ wow A ↑ Pi (B : Type) (T' A) (T' B) -> Wow
            • ⊢ B : Type
              • ⊢ B
                • result ⊢ B ↑ Type
              • ⊢ Type ≡ U'
              • ⊢ Type ≡ Type
              • result ⊢ B ↑ Type
            • result ⊢ wow A B ↑ T' A -> T' B -> Wow
          • ⊢ a : T' A
            • ⊢ a
              • result ⊢ a ↑ A
            • ⊢ A ≡ T' A
            • ⊢ T' A ≡ A
              • ⊢ Type ≡ Type
              • Hole solved!
            • result ⊢ a ↑ A
          • result ⊢ wow A B a ↑ _7 -> Wow
        • ⊢ a : _7
          • ⊢ a
            • result ⊢ a ↑ A
          • ⊢ A ≡ T' B
          • ⊢ A ≡ B
          • result ⊢ <a> ↑ _7
        • result ⊢ wow A B a <a> ↑ Wow
      • ⊢ Wow ≡ _6
      • ⊢ _6 ≡ Wow
        • ⊢ Type ≡ _6
        • Hole solved!
      • result ⊢ wow A B a <a> ↑ Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
  • ⊢ test2
    • result ⊢ test2 ↑ Pi {A B : Type} {A} {B} -> Wow
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment