search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

Positivity condition violation when using already-defined inductive datatype in definition of another inductive datatype #501

Open MM45 opened 11 months ago

MM45 commented 11 months ago

The following raises an error stating the datatype does not respect the positivity condition :

require import List.

type 'a tree = [
    Empty
  | Node of 'a & ('a tree) list
].

Swapping tree and list types around works just fine:

require import List.

type 'a tree = [
    Empty
  | Node of 'a & ('a list) tree
].