formality-pro-test.txt

import Nat@0
import Base

fold : {N : Ind2, ~A : Type, ~B : Type, id : !(A -> B), op : !(B -> B -> B)} -> ! {arr : Array(A, $ind2_depth(N))} -> B
  dup op   = op
  dup id   = id
  let moti = {n} Array(A, $ind2_depth(n)) -> B
  let step = {~n, a, b, arr}
    get [x, y] = arr
    op(a(x), b(y))
  let base = {n} id(n)
  dup fold = (use(N))(~moti, #step, #base)
  # {arr} fold(arr)
  
 #query.test : ![arr : Array(Word, 0n4), Word]
  let arr = [[[[0,1],[2,3]],[[4,5],[6,7]]], [[[8,9],[10,11]],[[12,13],[14,15]]]]
  let qry = {x} cpy x = x; [x, x .+. 100] // adds 100 to the element, returns the old value
  get [arr, a] = ($query*4)(~Word,  4, qry, arr)
  get [arr, b] = ($query*4)(~Word,  8, qry, arr)
  get [arr, c] = ($query*4)(~Word, 12, qry, arr)
  [arr, a .+. b .+. c]
  
  
f64_add : {case a : Double, case b : Double} -> Double
| f64 f64 => f64(a.value .++. b.value)

f64_sub : {case a : Double, case b : Double} -> Double
| f64 f64 => f64(a.value .--. b.value)

f64_mul : {case a : Double, case b : Double} -> Double
| f64 f64 => f64(a.value .**. b.value)

f64_div : {case a : Double, case b : Double} -> Double
| f64 f64 => f64(a.value .//. b.value)

f64_to_float : {case a : Double} -> Word
| f64 => a.value

f64_to_uint : {case a : Double} -> Word
| f64 => .u.(a.value)

f64_from_float : Word -> Double
 f64 

f64_from_uint : {a : Word} -> Double
  f64(.f.(a))
  
// Helper for reverse
#reverse.go*n :
  !{ ~T : Type
   , case halt list : List(T)
   , result : List(T)
   } -> List(T)
| cons  => reverse.go(~T, list.tail, cons(~T, list.head, result))
| nil   => result

N_Words : {n : Word} -> Type
  if n .<. 2:
    Word
  else:
    [:Word, N_Words(n .-. 1)]
    
annotation1
   [1, 2] :: [x : Word, (if x: Word else: Bool)]

#query_builder*N : !{~A : Type, path : Num, query : A -> [:A, A]} -> [path : Num, QueryBuilder(A, ($nat(N)))]
  get [abc, builder] = query_builder(~&A, path, query)
  cpy path_rest      = abc
  [path_rest .>>. 1, query_builder.succ(~&A, ~%($nat(+N)), path_rest .&. 1, builder)]
halt:
  [path, query_builder.zero(~&A, query)]
  
main : {f : Bool -> Nat} -> Nat
  log(f(true))
  ?a
  
main : Output
  print(everything)
  
main : {a : Bool, b : Bool} -> Bool
  case/Bool a
  + b : Bool
  | true  => b
  | false => not(b)
  : Bool
 
prove_1_is_2 : {e : Empty} -> Equal(Word, %1, %2)
  case/Empty e
  : Equal(Word, %1, %2)
  
 1 .#. 2
 1 .++. 2
 1 .--. 2
 1 .**. 2
 1 .//. 2
 1 .%%. 2
 1 .%. 2
 1 .^. 2 
 
 a .+. b
 a .-. b
 a .**. b
 a .#. 2
 a .++. 2
 a .--. 2
 a .**. 2
 a .//. 2
 a .%%. 2
 a .%. 2
 
// comment
#array.test : ![:Word, :Word, :Word, :Word, Word]
  // Prepares functions
  //Prepares funcstion
// Prepares functions
    // comment
  let cop = {x : Word} cpy x = x; [x, x]
  let set = set*8(~Word, #cop)
  let mut = mut*8(~Word, #cop) // comment
  let got = got*8(~Word, #cop)
  
 unstep_step_is_id : {i : Ind} -> ! Equal(Ind, %unstep(step(i)), %i)
  let motive = {i} &Equal(Ind, %unstep(step(i)), %i)
  let case_s = # {~n, h} cong(~Ind, ~Ind, ~%unstep(step(+n)), ~%+n, ~%step, h)
  dup F = (use(i))(~motive, case_s)
  # F(refl(~Ind, ~%base))

printado
loga
halti

: Double}-> Double