Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Not able to make literate agda file work #189

Open
spec-b opened this issue Aug 24, 2024 · 0 comments
Open

Not able to make literate agda file work #189

spec-b opened this issue Aug 24, 2024 · 0 comments

Comments

@spec-b
Copy link

spec-b commented Aug 24, 2024

Hi, So I was trying to type check and compile an agda file and it was throwing up a lot of errors, so I took a part of the beginning which is this:
{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module hott-uftry1 where

open import Universes public

variable
𝓤 𝓥 𝓦 𝓣 : Universe

data 𝟙 : 𝓤₀ ̇ where
⋆ : 𝟙

And I tried to type check and compile. But it gives the error that it cannot find the source of module Universes in any of the stdlib when scope checking the declaration open import Universes public.

There is a literate agda file which has this content and much more. But it wasn't type checking or compiling either. I'm worried is this a unicode issue because it works fine(?) in emacs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant