Skip to content

Commit

Permalink
class: add more test
Browse files Browse the repository at this point in the history
  • Loading branch information
HoshinoTented committed Jul 7, 2024
1 parent 3218d25 commit 8e33f0c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion cli-impl/src/test/resources/success/src/Classes.aya
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@ class Kontainer

def tyck0 : Nat => Kontainer::walue {new Kontainer Nat 0}

// def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl
def norm0 : Kontainer::walue {new Kontainer Nat 0} = 0 => refl

0 comments on commit 8e33f0c

Please sign in to comment.