Skip to content

Instantly share code, notes, and snippets.

@pnlph

pnlph/#3135.agda

Last active May 10, 2020 16:11
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save pnlph/40cd474004cb40aa25d489ad37c79fb2 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save pnlph/40cd474004cb40aa25d489ad37c79fb2 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. pnlph revised this gist May 10, 2020. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion #3135.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -12,7 +12,7 @@ postulate

    open import Agda.Builtin.Equality using (_≡_ ; refl)
    _ : A □ ≡ A □
    _ = ref
    _ = refl

    -- C-c C-l fails (version 2.6.1)
    -- Don't know how to parse A □ ≡ A □. Could mean any one of:
  2. pnlph revised this gist May 10, 2020. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion #3135.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,6 @@
    module issue.#3135 where

    -- \sqw
    -- latex \sqw
    postulate
    A : Set
    □ : Set
  3. pnlph revised this gist May 10, 2020. 1 changed file with 3 additions and 3 deletions.
    6 changes: 3 additions & 3 deletions #3135.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,6 @@
    module issue.#3135 where

    -- latex \sqw
    -- \sqw
    postulate
    A : Set
    □ : Set
    @@ -14,9 +14,9 @@ open import Agda.Builtin.Equality using (_≡_ ; refl)
    _ : A □ ≡ A □
    _ = ref

    -- C-c C-l fails
    -- C-c C-l fails (version 2.6.1)
    -- Don't know how to parse A □ ≡ A □. Could mean any one of:
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
  4. pnlph created this gist May 10, 2020.
    22 changes: 22 additions & 0 deletions #3135.agda
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,22 @@
    module issue.#3135 where

    -- latex \sqw
    postulate
    A : Set
    □ : Set
    _□ : Set → Set
    ⟨_⟩ : Set → Set

    --G : Set
    --G = ? □

    open import Agda.Builtin.Equality using (_≡_ ; refl)
    _ : A □ ≡ A □
    _ = ref

    -- C-c C-l fails
    -- Don't know how to parse A □ ≡ A □. Could mean any one of:
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)
    -- (A □) ≡ (A □)