Skip to main content

Browse the archive

Revision 445254861f733c4d5a0c852383bdf9a5058086bd authored by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC, committed by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC 
Unfuck doctests
1 parent 097f354
Raw File
contra.fq 
fixpoint "--rewrite"

constant sem: (func(0, [int; int; (Set_Set int)]))

define sem (i : int,  j: int) : (Set_Set int) = (&& [((sem i j) = (if (i < j) then (Set_cup (Set_add (Set_empty 0) i) (sem (i + 1) j)) else (Set_empty 0)));
                                                              (true => true)])

expand [1 : True]

bind 1 i0 : { v : int | true    }
bind 2 j0 : { v : int | true    }
bind 3 p  : { v : int | i0 < j0 }
bind 4 q  : { v : int | j0 < i0 }

constraint:
  env [1; 2; 3; 4]
  lhs {v : (Set_Set int) | v = sem i0 j0}
  rhs {v : (Set_Set int) | v = sem j0 i0}
  id 1 tag []
back to top