search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
442 stars 54 forks source link

Bug with record patterns #2801

Closed janmasrovira closed 4 weeks ago

janmasrovira commented 4 weeks ago

The following should type check:

type Pair (A B : Type) :=
  mkPair {
    fst : A;
    snd : B
  };

type T := t;

partialMatch : Pair T T -> T
  | mypair@mkPair@{snd := t} := t;