fabianhjr

module Naturales

data Natural : Type where
  Cero : Natural
  Sucesor : Natural -> Natural

-- Prop

public export
suma : Natural -> Natural -> Natural

fabianhjr

export
notTrueIsFalse : not True = False
notTrueIsFalse = Refl

interface Preorder a where
  (≲) : a → a → Bool
  x ≲ y = not (x ≴ y)
  (≴) : a → a → Bool
  x ≴ y = not (x ≲ y)

fabianhjr

module Test

import Prelude.List

mutual
  data Trie : Type where
    Empty : Trie
    Node : Char -> Trie -> Trie
    Arc : (l: List Trie) -> {auto ok: AreNodes l} -> Trie

fabianhjr

### Keybase proof

I hereby claim:

  * I am fabianhjr on github.
  * I am fabianhjr (https://keybase.io/fabianhjr) on keybase.
  * I have a public key ASC2c2imFP92jXMT_ECBEmWbpKGsIyBykFc15jN6-mPMawo

To claim this, I am signing this object:

fabianhjr

\documentclass[spanish,]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex

fabianhjr

;; -*- mode: emacs-lisp -*-
;; This file is loaded by Spacemacs at startup.
;; It must be stored in your home directory.

(defun dotspacemacs/layers ()
  "Configuration Layers declaration.
You should not put any user code in this function besides modifying the variable
values."
  (setq-default
   ;; Base distribution to use. This is a layer contained in the directory

fabianhjr

@font-face {
    font-family: 'firacode';
    font-weight: normal;
    font-style: normal;
    src: url('https://cdn.rawgit.com/tonsky/FiraCode/436ac320b39184d91ea9b0e246223663a5f6fbf2/distr/otf/FiraCode-Retina.otf');
}
    
.hljs {
    font-family: 'firacode' !important;
}

fabianhjr

example :: Eq a => a
example = (1 :: Int)

fabianhjr

homeassistant/util/__init__.py:320: error: "module" has no attribute "PriorityQueue"
homeassistant/util/package.py:34: error: "module" has no attribute "SubprocessError"
homeassistant/util/package.py:59: error: Iterable expected
homeassistant/scripts/macos.py:17: error: Incompatible types in assignment (expression has type IO[Any], variable has type "TextIO")
homeassistant/helpers/event.py:88: error: Callable[..., Any] has no attribute "run"
homeassistant/loader.py:44: error: "module" has no attribute "__path__"
homeassistant/helpers/config_validation.py:353: error: Cannot determine type of 'CONDITION_SCHEMA'
homeassistant/helpers/config_validation.py:362: error: Cannot determine type of 'CONDITION_SCHEMA'
homeassistant/config.py:107: error: Cannot determine type of 'DEFAULT_CONFIG'
homeassistant/config.py:115: error: Cannot determine type of 'DEFAULT_CONFIG'

fabianhjr

Java (Groovy, Scala, Clojure, Kotlin) ; The Javas
C (C++, D, Rust, Nim) ; System Programming
Python (Coconut) | Ruby | Crystal | Io | Smalltalk ; Multis/OOPs
JavaScript (Dart, Scala.js, Elm, ClojureScript, CoffeeScript) ; The Browser Languages
Assembly (x86, ARM, PowerPC, RISC-V) ; Assemblers
R | Sage ; Math
Perl | Lua ; Sysadmin/Scripting
Lisp (Scheme, Common Lisp, Emacs Lisp) ; Lisps
Prolog ; Logic Programming
Erlang (Elixir, LFE) | Go ; Concurrent/Distributed