Skip to content

Commit

Permalink
fix: ture
Browse files Browse the repository at this point in the history
  • Loading branch information
HoshinoTented committed Dec 29, 2024
1 parent e49b067 commit 6253f37
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions cli-impl/src/test/resources/shared/src/data/vec/base.aya
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
open import prelude hiding (++)

@suppress(Shadowing)
open inductive Vec (n : Nat) (A : Type) elim n
| 0 => []
| suc n => infixr :> A (Vec n A)
Expand Down

0 comments on commit 6253f37

Please sign in to comment.