tsani

all' : (a -> Bool) -> List a -> Bool
all' f [] = True
all' f (x :: xs) = f x && all' f xs
  
allLemma : f x = True -> all' f xs = True -> all' f (x :: xs) = True
allLemma p1 p2 = rewrite p1 in rewrite p2 in Refl
  
allFiltered : (f : a -> Bool) -> (xs : List a) -> all' f (filter f xs) = True
allFiltered f [] = Refl
allFiltered f (x :: xs) = lemma (allFiltered f xs) (f x) Refl where

tsani

module false 

%default total

data V : Type where
  Lam : ({a : Type} -> a -> a) -> V
  
t : V
t = Lam id
  

tsani

@Function                                                                                                                                                                 
def partition(f, xs):                                                              
    """ Partition a sequence according to satisfaction of a predicate.             
                                                                                   
    The result is a tuple in which the first component is a sequence of            
    unsatisfying elements and the second is a sequence of satisfying elements.  
    """                                                                            
    result = ([], [])                                                              
    for x in xs:                                                                   
        result[1 if f(x) else 0].append(x)                                         

tsani

Keybase proof

I hereby claim:

• I am tsani on github.
• I am tsani (https://keybase.io/tsani) on keybase.
• I have a public key whose fingerprint is 1809 A414 7F27 58CD 2058 2714 42A2 429F 3344 69DF

To claim this, I am signing this object:

tsani

module OpenUniverse

data IntSpec : Type where
  INT : IntSpec

data StringSpec : Type where
  STRING : StringSpec

interface Interpolation (a : Type) where
  total

tsani

# It's tough to give a truly temporary name to a value in Python. 

# Of course, we can just do something like
t = my_complicated_expression
v = do_stuff_with(t) + do_different_stuff_with(t)

# and now "t" has whatever value "my_complicated_expression" evaluates to, 
# but this requires a separate statement altogether, which makes reusing 
# the result of a complicated evaluation several times in a lambda function 
# impossible.

tsani

glibau po'o
===========

Johnny: Just look at ‘em… Did you know there were so many lights in the sky?
River: Yes.
Johnny: Oh… Uh, I did too.  You said this was your spot, right?
River: Only during the carnival.
Johnny: Not a fan of the crowds?  … Me neither.  Y’know, you still haven’t told me your name yet.
River: I’m not telling you. … Everyone makes fun of it in school.
Johnny: Why?