1 kyu

Two paths in the forest

33lwoo1999
Description
Loading description...
Theorem Proving
Fundamentals
View
AllIssues2QuestionsSuggestions1Show Resolved
  • Please sign in or sign up to leave a comment.
  • andersk Avatar

    Agda test cases should not open the solution; that can often be exploited to bring unexpected definitions into scope.

  • monadius Avatar

    Approved

  • ice1000 Avatar

    This is definitely 1kyu. Cool Kata!!

  • ice1000 Avatar

    Do I need these 3 imports?

    open import Level
open import Cubical.Core.Everything
open import Cubical.Data.Bool

    these imports give me error.

    • ice1000 Avatar

      Lift Bool should be Lift _ Bool

    • lwoo1999 Avatar

      Sorry, I forgot to add import in the initial solution.

      open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Data.Everything

      Level is not necessary for Cubical.Core.Primitives reimports builtin level and level in stdlib may be not compatible.

      Lift is in Cubical.Foundations.Univalence:

      record Lift {i j} (A : Set i) : Set (ℓ-max i j) where
  instance constructor lift
  field
    lower : A

      i j are both implicit so Lift Bool is just OK.

      Issue marked resolved by lwoo1999 6 years ago
  • ice1000 Avatar

    ℓ-max not in scope, should add import